Theorem cgrcomlrand

Description: Deduction form of cgrcomlr . (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	cgrcomlrand	$$⊢\left(\phi \wedge \psi \right)\to ⟨B,A⟩\mathrm{Cgr}⟨D,C⟩$$

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	1 2 3 4 5 6	cgrcomrand	$$⊢\left(\phi \wedge \psi \right)\to ⟨A,B⟩\mathrm{Cgr}⟨D,C⟩$$
8	1 2 3 5 4 7	cgrcomland	$$⊢\left(\phi \wedge \psi \right)\to ⟨B,A⟩\mathrm{Cgr}⟨D,C⟩$$