Theorem cgrcomlrand

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

	Ref	Expression
Hypotheses	cgrcomlrand.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	cgrcomlrand.2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrcomlrand.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrcomlrand.4	⊢ ( 𝜑 → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrcomlrand.5	⊢ ( 𝜑 → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
	cgrcomlrand.6	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
Assertion	cgrcomlrand	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐵 , 𝐴 ⟩ 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	1 2 3 4 5 6	cgrcomrand	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐶 ⟩ )
8	1 2 3 5 4 7	cgrcomland	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐷 , 𝐶 ⟩ )