Theorem cgrcomland

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

	Ref	Expression
Hypotheses	cgrcomlrand.1	$$⊢\phi \to N\in \mathbb{N}$$
	cgrcomlrand.2	$$⊢\phi \to A\in 𝔼\left(N\right)$$
	cgrcomlrand.3	$$⊢\phi \to B\in 𝔼\left(N\right)$$
	cgrcomlrand.4	$$⊢\phi \to C\in 𝔼\left(N\right)$$
	cgrcomlrand.5	$$⊢\phi \to D\in 𝔼\left(N\right)$$
	cgrcomlrand.6	$$⊢\left(\phi \wedge \psi \right)\to ⟨A,B⟩\mathrm{Cgr}⟨C,D⟩$$
Assertion	cgrcomland	$$⊢\left(\phi \wedge \psi \right)\to ⟨B,A⟩\mathrm{Cgr}⟨C,D⟩$$

Proof

Step	Hyp	Ref	Expression
1		cgrcomlrand.1	$$⊢\phi \to N\in \mathbb{N}$$
2		cgrcomlrand.2	$$⊢\phi \to A\in 𝔼\left(N\right)$$
3		cgrcomlrand.3	$$⊢\phi \to B\in 𝔼\left(N\right)$$
4		cgrcomlrand.4	$$⊢\phi \to C\in 𝔼\left(N\right)$$
5		cgrcomlrand.5	$$⊢\phi \to D\in 𝔼\left(N\right)$$
6		cgrcomlrand.6	$$⊢\left(\phi \wedge \psi \right)\to ⟨A,B⟩\mathrm{Cgr}⟨C,D⟩$$
7		cgrcoml	$$⊢\left(N\in \mathbb{N}\wedge \left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\wedge \left(C\in 𝔼\left(N\right)\wedge D\in 𝔼\left(N\right)\right)\right)\to \left(⟨A,B⟩\mathrm{Cgr}⟨C,D⟩\leftrightarrow ⟨B,A⟩\mathrm{Cgr}⟨C,D⟩\right)$$
8	1 2 3 4 5 7	syl122anc	$$⊢\phi \to \left(⟨A,B⟩\mathrm{Cgr}⟨C,D⟩\leftrightarrow ⟨B,A⟩\mathrm{Cgr}⟨C,D⟩\right)$$
9	8	adantr	$$⊢\left(\phi \wedge \psi \right)\to \left(⟨A,B⟩\mathrm{Cgr}⟨C,D⟩\leftrightarrow ⟨B,A⟩\mathrm{Cgr}⟨C,D⟩\right)$$
10	6 9	mpbid	$$⊢\left(\phi \wedge \psi \right)\to ⟨B,A⟩\mathrm{Cgr}⟨C,D⟩$$