linecgrand

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

Step	Hyp	Ref	Expression
1		linecgrand.1	$⊢ φ \to N \in ℕ$
2		linecgrand.2	$⊢ φ \to A \in 𝔼 (N)$
3		linecgrand.3	$⊢ φ \to B \in 𝔼 (N)$
4		linecgrand.4	$⊢ φ \to C \in 𝔼 (N)$
5		linecgrand.5	$⊢ φ \to P \in 𝔼 (N)$
6		linecgrand.6	$⊢ φ \to Q \in 𝔼 (N)$
7		linecgrand.7	$⊢ (φ \land ψ) \to A \neq B$
8		linecgrand.8	$⊢ (φ \land ψ) \to A Colinear ⟨B, C⟩$
9		linecgrand.9	$⊢ (φ \land ψ) \to ⟨A, P⟩ Cgr ⟨A, Q⟩$
10		linecgrand.10	$⊢ (φ \land ψ) \to ⟨B, P⟩ Cgr ⟨B, Q⟩$
11	7 8	jca	$⊢ (φ \land ψ) \to (A \neq B \land A Colinear ⟨B, C⟩)$
12	9 10	jca	$⊢ (φ \land ψ) \to (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)$
13		linecgr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)) \to ⟨C, P⟩ Cgr ⟨C, Q⟩)$
14	1 2 3 4 5 6 13	syl132anc	$⊢ φ \to (((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)) \to ⟨C, P⟩ Cgr ⟨C, Q⟩)$
15	14	adantr	$⊢ (φ \land ψ) \to (((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)) \to ⟨C, P⟩ Cgr ⟨C, Q⟩)$
16	11 12 15	mp2and	$⊢ (φ \land ψ) \to ⟨C, P⟩ Cgr ⟨C, Q⟩$

Metamath Proof Explorer