Metamath Proof Explorer

Theorem cgrtrand

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

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

Proof

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