Theorem cgrextendand

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

	Ref	Expression
Hypotheses	cgrextendand.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	cgrextendand.2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrextendand.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrextendand.4	⊢ ( 𝜑 → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrextendand.5	⊢ ( 𝜑 → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrextendand.6	⊢ ( 𝜑 → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrextendand.7	⊢ ( 𝜑 → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrextendand.8	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
	cgrextendand.9	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ )
	cgrextendand.10	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ )
	cgrextendand.11	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ )
Assertion	cgrextendand	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		cgrextendand.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		cgrextendand.2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3		cgrextendand.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
4		cgrextendand.4	⊢ ( 𝜑 → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
5		cgrextendand.5	⊢ ( 𝜑 → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
6		cgrextendand.6	⊢ ( 𝜑 → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
7		cgrextendand.7	⊢ ( 𝜑 → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
8		cgrextendand.8	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
9		cgrextendand.9	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ )
10		cgrextendand.10	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ )
11		cgrextendand.11	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ )
12	8 9	jca	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) )
13	10 11	jca	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) )
14		cgrextend	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) )
15	1 2 3 4 5 6 7 14	syl133anc	⊢ ( 𝜑 → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) )
17	12 13 16	mp2and	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ )