Theorem cgrcomland

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

	Ref	Expression
Hypotheses	cgrcomlrand.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	cgrcomlrand.2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrcomlrand.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrcomlrand.4	⊢ ( 𝜑 → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrcomlrand.5	⊢ ( 𝜑 → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrcomlrand.6	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
Assertion	cgrcomland	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		cgrcomlrand.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		cgrcomlrand.2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3		cgrcomlrand.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
4		cgrcomlrand.4	⊢ ( 𝜑 → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
5		cgrcomlrand.5	⊢ ( 𝜑 → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
6		cgrcomlrand.6	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
7		cgrcoml	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
8	1 2 3 4 5 7	syl122anc	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
10	6 9	mpbid	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )