# 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$