Theorem cgrtrand

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

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

Proof

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