Metamath Proof Explorer

Theorem cgrcomrand

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

Ref Expression
Hypotheses cgrcomlrand.1 ${⊢}{\phi }\to {N}\in ℕ$
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 cgrcomrand ${⊢}\left({\phi }\wedge {\psi }\right)\to ⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{C}⟩$

Proof

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