Theorem cgrcomand

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

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

Proof

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