6gbe

		Ref	Expression
	Assertion	6gbe	$⊢ 6 \in GoldbachEven$

Step	Hyp	Ref	Expression
1		6even	$⊢ 6 \in Even$
2		3prm	$⊢ 3 \in ℙ$
3		3odd	$⊢ 3 \in Odd$
4		gbpart6	$⊢ 6 = 3 + 3$
5	3 3 4	3pm3.2i	$⊢ (3 \in Odd \land 3 \in Odd \land 6 = 3 + 3)$
6		eleq1	$⊢ p = 3 \to (p \in Odd \leftrightarrow 3 \in Odd)$
7		biidd	$⊢ p = 3 \to (q \in Odd \leftrightarrow q \in Odd)$
8		oveq1	$⊢ p = 3 \to p + q = 3 + q$
9	8	eqeq2d	$⊢ p = 3 \to (6 = p + q \leftrightarrow 6 = 3 + q)$
10	6 7 9	3anbi123d	$⊢ p = 3 \to ((p \in Odd \land q \in Odd \land 6 = p + q) \leftrightarrow (3 \in Odd \land q \in Odd \land 6 = 3 + q))$
11		biidd	$⊢ q = 3 \to (3 \in Odd \leftrightarrow 3 \in Odd)$
12		eleq1	$⊢ q = 3 \to (q \in Odd \leftrightarrow 3 \in Odd)$
13		oveq2	$⊢ q = 3 \to 3 + q = 3 + 3$
14	13	eqeq2d	$⊢ q = 3 \to (6 = 3 + q \leftrightarrow 6 = 3 + 3)$
15	11 12 14	3anbi123d	$⊢ q = 3 \to ((3 \in Odd \land q \in Odd \land 6 = 3 + q) \leftrightarrow (3 \in Odd \land 3 \in Odd \land 6 = 3 + 3))$
16	10 15	rspc2ev	$⊢ (3 \in ℙ \land 3 \in ℙ \land (3 \in Odd \land 3 \in Odd \land 6 = 3 + 3)) \to \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land 6 = p + q)$
17	2 2 5 16	mp3an	$⊢ \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land 6 = p + q)$
18		isgbe	$⊢ 6 \in GoldbachEven \leftrightarrow (6 \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land 6 = p + q))$
19	1 17 18	mpbir2an	$⊢ 6 \in GoldbachEven$

Metamath Proof Explorer