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 ⊢ φ ∧ ψ → A B Cgr C D
cgrtr4and.9 ⊢ φ ∧ ψ → A B Cgr E F
Assertion cgrtr4and ⊢ φ ∧ ψ → C D Cgr E F

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 ⊢ φ ∧ ψ → A B Cgr C D
9 cgrtr4and.9 ⊢ φ ∧ ψ → A B Cgr E F
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 ⊢ φ ∧ ψ → C D Cgr E F