Metamath Proof Explorer

Theorem sbgoldbb

Description: If the strong binary Goldbach conjecture is valid, the binary Goldbach conjecture is valid. (Contributed by AV, 23-Dec-2021)

Ref Expression
Assertion sbgoldbb ⊢∀n∈Even4<n→n∈GoldbachEven→∀n∈Even2<n→∃p∈ℙ∃q∈ℙn=p+q

Proof

Step Hyp Ref Expression
1 sbgoldbalt ⊢∀n∈Even4<n→n∈GoldbachEven↔∀n∈Even2<n→∃p∈ℙ∃q∈ℙn=p+q
2 1 biimpi ⊢∀n∈Even4<n→n∈GoldbachEven→∀n∈Even2<n→∃p∈ℙ∃q∈ℙn=p+q