cgrextendand

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

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

Metamath Proof Explorer