Metamath Proof Explorer


Theorem cgrcomand

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

Ref Expression
Hypotheses cgrcomand.1 φ N
cgrcomand.2 φ A 𝔼 N
cgrcomand.3 φ B 𝔼 N
cgrcomand.4 φ C 𝔼 N
cgrcomand.5 φ D 𝔼 N
cgrcomand.6 φ ψ A B Cgr C D
Assertion cgrcomand φ ψ C D Cgr A B

Proof

Step Hyp Ref Expression
1 cgrcomand.1 φ N
2 cgrcomand.2 φ A 𝔼 N
3 cgrcomand.3 φ B 𝔼 N
4 cgrcomand.4 φ C 𝔼 N
5 cgrcomand.5 φ D 𝔼 N
6 cgrcomand.6 φ ψ A B Cgr C D
7 cgrcom N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B Cgr C D C D Cgr A B
8 1 2 3 4 5 7 syl122anc φ A B Cgr C D C D Cgr A B
9 8 adantr φ ψ A B Cgr C D C D Cgr A B
10 6 9 mpbid φ ψ C D Cgr A B