Theorem cgrtr4d

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

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

Proof

Step	Hyp	Ref	Expression
1		cgrtr4d.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		cgrtr4d.2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3		cgrtr4d.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
4		cgrtr4d.4	⊢ ( 𝜑 → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
5		cgrtr4d.5	⊢ ( 𝜑 → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
6		cgrtr4d.6	⊢ ( 𝜑 → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
7		cgrtr4d.7	⊢ ( 𝜑 → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
8		cgrtr4d.8	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
9		cgrtr4d.9	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ )
10		axcgrtr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) )
11	1 2 3 4 5 6 7 10	syl133anc	⊢ ( 𝜑 → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) )
12	8 9 11	mp2and	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ )