cgrtr3and

Description: Deduction form of cgrtr3 . (Contributed by Scott Fenton, 13-Oct-2013)

Step	Hyp	Ref	Expression
1		cgrtr3and.1	$⊢ φ \to N \in ℕ$
2		cgrtr3and.2	$⊢ φ \to A \in 𝔼 (N)$
3		cgrtr3and.3	$⊢ φ \to B \in 𝔼 (N)$
4		cgrtr3and.4	$⊢ φ \to C \in 𝔼 (N)$
5		cgrtr3and.5	$⊢ φ \to D \in 𝔼 (N)$
6		cgrtr3and.6	$⊢ φ \to E \in 𝔼 (N)$
7		cgrtr3and.7	$⊢ φ \to F \in 𝔼 (N)$
8		cgrtr3and.8	$⊢ (φ \land ψ) \to ⟨A, B⟩ Cgr ⟨E, F⟩$
9		cgrtr3and.9	$⊢ (φ \land ψ) \to ⟨C, D⟩ Cgr ⟨E, F⟩$
10		cgrtr3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, F⟩) \to ⟨A, B⟩ Cgr ⟨C, D⟩)$
11	1 2 3 4 5 6 7 10	syl133anc	$⊢ φ \to ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, F⟩) \to ⟨A, B⟩ Cgr ⟨C, D⟩)$
12	11	adantr	$⊢ (φ \land ψ) \to ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, F⟩) \to ⟨A, B⟩ Cgr ⟨C, D⟩)$
13	8 9 12	mp2and	$⊢ (φ \land ψ) \to ⟨A, B⟩ Cgr ⟨C, D⟩$

Metamath Proof Explorer