Theorem cgrtr4and

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

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

Proof

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