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	\|- ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )

Step	Hyp	Ref	Expression
1		sbgoldbalt	\|- ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) <-> A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
2	1	biimpi	\|- ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )

Step

Hyp

Ref

Expression

 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) <-> A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )

 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )