cgrtrand

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

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

Metamath Proof Explorer