Metamath Proof Explorer

Theorem cgrtr3and

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

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

Proof

Step Hyp Ref Expression
1 cgrtr3and.1 ⊢ φ → N ∈ ℕ
2 cgrtr3and.2 ⊢ φ → A ∈ 𝔼 ⁡ N
3 cgrtr3and.3 ⊢ φ → B ∈ 𝔼 ⁡ N
4 cgrtr3and.4 ⊢ φ → C ∈ 𝔼 ⁡ N
5 cgrtr3and.5 ⊢ φ → D ∈ 𝔼 ⁡ N
6 cgrtr3and.6 ⊢ φ → E ∈ 𝔼 ⁡ N
7 cgrtr3and.7 ⊢ φ → F ∈ 𝔼 ⁡ N
8 cgrtr3and.8 ⊢ φ ∧ ψ → A B Cgr E F
9 cgrtr3and.9 ⊢ φ ∧ ψ → C D Cgr E F
10 cgrtr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B Cgr E F ∧ C D Cgr E F → A B Cgr C D
11 1 2 3 4 5 6 7 10 syl133anc ⊢ φ → A B Cgr E F ∧ C D Cgr E F → A B Cgr C D
12 11 adantr ⊢ φ ∧ ψ → A B Cgr E F ∧ C D Cgr E F → A B Cgr C D
13 8 9 12 mp2and ⊢ φ ∧ ψ → A B Cgr C D