Metamath Proof Explorer

Theorem cgrextendand

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

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

Proof

Step Hyp Ref Expression
1 cgrextendand.1 ⊢ φ → N ∈ ℕ
2 cgrextendand.2 ⊢ φ → A ∈ 𝔼 ⁡ N
3 cgrextendand.3 ⊢ φ → B ∈ 𝔼 ⁡ N
4 cgrextendand.4 ⊢ φ → C ∈ 𝔼 ⁡ N
5 cgrextendand.5 ⊢ φ → D ∈ 𝔼 ⁡ N
6 cgrextendand.6 ⊢ φ → E ∈ 𝔼 ⁡ N
7 cgrextendand.7 ⊢ φ → F ∈ 𝔼 ⁡ N
8 cgrextendand.8 ⊢ φ ∧ ψ → B Btwn A C
9 cgrextendand.9 ⊢ φ ∧ ψ → E Btwn D F
10 cgrextendand.10 ⊢ φ ∧ ψ → A B Cgr D E
11 cgrextendand.11 ⊢ φ ∧ ψ → B C Cgr E F
12 8 9 jca ⊢ φ ∧ ψ → B Btwn A C ∧ E Btwn D F
13 10 11 jca ⊢ φ ∧ ψ → A B Cgr D E ∧ B C Cgr E F
14 cgrextend ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B Btwn A C ∧ E Btwn D F ∧ A B Cgr D E ∧ B C Cgr E F → A C Cgr D F
15 1 2 3 4 5 6 7 14 syl133anc ⊢ φ → B Btwn A C ∧ E Btwn D F ∧ A B Cgr D E ∧ B C Cgr E F → A C Cgr D F
16 15 adantr ⊢ φ ∧ ψ → B Btwn A C ∧ E Btwn D F ∧ A B Cgr D E ∧ B C Cgr E F → A C Cgr D F
17 12 13 16 mp2and ⊢ φ ∧ ψ → A C Cgr D F