Theorem linecgrand

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

	Ref	Expression
Hypotheses	linecgrand.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	linecgrand.2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
	linecgrand.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
	linecgrand.4	⊢ ( 𝜑 → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
	linecgrand.5	⊢ ( 𝜑 → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
	linecgrand.6	⊢ ( 𝜑 → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
	linecgrand.7	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 ≠ 𝐵 )
	linecgrand.8	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ )
	linecgrand.9	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ )
	linecgrand.10	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ )
Assertion	linecgrand	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑄 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		linecgrand.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		linecgrand.2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3		linecgrand.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
4		linecgrand.4	⊢ ( 𝜑 → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
5		linecgrand.5	⊢ ( 𝜑 → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
6		linecgrand.6	⊢ ( 𝜑 → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
7		linecgrand.7	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 ≠ 𝐵 )
8		linecgrand.8	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ )
9		linecgrand.9	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ )
10		linecgrand.10	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ )
11	7 8	jca	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) )
12	9 10	jca	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) )
13		linecgr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑄 ⟩ ) )
14	1 2 3 4 5 6 13	syl132anc	⊢ ( 𝜑 → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑄 ⟩ ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑄 ⟩ ) )
16	11 12 15	mp2and	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑄 ⟩ )