Metamath Proof Explorer

Theorem cgrtr4and

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

Ref Expression
Hypotheses cgrtr4and.1 ⊢φ→N∈ℕ
cgrtr4and.2 ⊢φ→A∈𝔼⁡N
cgrtr4and.3 ⊢φ→B∈𝔼⁡N
cgrtr4and.4 ⊢φ→C∈𝔼⁡N
cgrtr4and.5 ⊢φ→D∈𝔼⁡N
cgrtr4and.6 ⊢φ→E∈𝔼⁡N
cgrtr4and.7 ⊢φ→F∈𝔼⁡N
cgrtr4and.8 ⊢φ∧ψ→ABCgrCD
cgrtr4and.9 ⊢φ∧ψ→ABCgrEF
Assertion cgrtr4and ⊢φ∧ψ→CDCgrEF

Proof

Step Hyp Ref Expression
1 cgrtr4and.1 ⊢φ→N∈ℕ
2 cgrtr4and.2 ⊢φ→A∈𝔼⁡N
3 cgrtr4and.3 ⊢φ→B∈𝔼⁡N
4 cgrtr4and.4 ⊢φ→C∈𝔼⁡N
5 cgrtr4and.5 ⊢φ→D∈𝔼⁡N
6 cgrtr4and.6 ⊢φ→E∈𝔼⁡N
7 cgrtr4and.7 ⊢φ→F∈𝔼⁡N
8 cgrtr4and.8 ⊢φ∧ψ→ABCgrCD
9 cgrtr4and.9 ⊢φ∧ψ→ABCgrEF
10 1 adantr ⊢φ∧ψ→N∈ℕ
11 2 adantr ⊢φ∧ψ→A∈𝔼⁡N
12 3 adantr ⊢φ∧ψ→B∈𝔼⁡N
13 4 adantr ⊢φ∧ψ→C∈𝔼⁡N
14 5 adantr ⊢φ∧ψ→D∈𝔼⁡N
15 6 adantr ⊢φ∧ψ→E∈𝔼⁡N
16 7 adantr ⊢φ∧ψ→F∈𝔼⁡N
17 10 11 12 13 14 15 16 8 9 cgrtr4d ⊢φ∧ψ→CDCgrEF