Theorem cgrcomand

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

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

Proof

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