Metamath Proof Explorer

Theorem linecgrand

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

Ref Expression
Hypotheses linecgrand.1 ⊢ φ → N ∈ ℕ
linecgrand.2 ⊢ φ → A ∈ 𝔼 ⁡ N
linecgrand.3 ⊢ φ → B ∈ 𝔼 ⁡ N
linecgrand.4 ⊢ φ → C ∈ 𝔼 ⁡ N
linecgrand.5 ⊢ φ → P ∈ 𝔼 ⁡ N
linecgrand.6 ⊢ φ → Q ∈ 𝔼 ⁡ N
linecgrand.7 ⊢ φ ∧ ψ → A ≠ B
linecgrand.8 ⊢ φ ∧ ψ → A Colinear B C
linecgrand.9 ⊢ φ ∧ ψ → A P Cgr A Q
linecgrand.10 ⊢ φ ∧ ψ → B P Cgr B Q
Assertion linecgrand ⊢ φ ∧ ψ → C P Cgr C Q

Proof

Step Hyp Ref Expression
1 linecgrand.1 ⊢ φ → N ∈ ℕ
2 linecgrand.2 ⊢ φ → A ∈ 𝔼 ⁡ N
3 linecgrand.3 ⊢ φ → B ∈ 𝔼 ⁡ N
4 linecgrand.4 ⊢ φ → C ∈ 𝔼 ⁡ N
5 linecgrand.5 ⊢ φ → P ∈ 𝔼 ⁡ N
6 linecgrand.6 ⊢ φ → Q ∈ 𝔼 ⁡ N
7 linecgrand.7 ⊢ φ ∧ ψ → A ≠ B
8 linecgrand.8 ⊢ φ ∧ ψ → A Colinear B C
9 linecgrand.9 ⊢ φ ∧ ψ → A P Cgr A Q
10 linecgrand.10 ⊢ φ ∧ ψ → B P Cgr B Q
11 7 8 jca ⊢ φ ∧ ψ → A ≠ B ∧ A Colinear B C
12 9 10 jca ⊢ φ ∧ ψ → A P Cgr A Q ∧ B P Cgr B Q
13 linecgr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N → A ≠ B ∧ A Colinear B C ∧ A P Cgr A Q ∧ B P Cgr B Q → C P Cgr C Q
14 1 2 3 4 5 6 13 syl132anc ⊢ φ → A ≠ B ∧ A Colinear B C ∧ A P Cgr A Q ∧ B P Cgr B Q → C P Cgr C Q
15 14 adantr ⊢ φ ∧ ψ → A ≠ B ∧ A Colinear B C ∧ A P Cgr A Q ∧ B P Cgr B Q → C P Cgr C Q
16 11 12 15 mp2and ⊢ φ ∧ ψ → C P Cgr C Q