Metamath Proof Explorer

Theorem linecgrand

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

Ref Expression
Hypotheses linecgrand.1 
|- ( ph -> N e. NN )
linecgrand.2 
|- ( ph -> A e. ( EE ` N ) )
linecgrand.3 
|- ( ph -> B e. ( EE ` N ) )
linecgrand.4 
|- ( ph -> C e. ( EE ` N ) )
linecgrand.5 
|- ( ph -> P e. ( EE ` N ) )
linecgrand.6 
|- ( ph -> Q e. ( EE ` N ) )
linecgrand.7 
|- ( ( ph /\ ps ) -> A =/= B )
linecgrand.8 
|- ( ( ph /\ ps ) -> A Colinear <. B , C >. )
linecgrand.9 
|- ( ( ph /\ ps ) -> <. A , P >. Cgr <. A , Q >. )
linecgrand.10 
|- ( ( ph /\ ps ) -> <. B , P >. Cgr <. B , Q >. )
Assertion linecgrand 
|- ( ( ph /\ ps ) -> <. C , P >. Cgr <. C , Q >. )

Proof

Step Hyp Ref Expression
1 linecgrand.1 
 |-  ( ph -> N e. NN )
2 linecgrand.2 
 |-  ( ph -> A e. ( EE ` N ) )
3 linecgrand.3 
 |-  ( ph -> B e. ( EE ` N ) )
4 linecgrand.4 
 |-  ( ph -> C e. ( EE ` N ) )
5 linecgrand.5 
 |-  ( ph -> P e. ( EE ` N ) )
6 linecgrand.6 
 |-  ( ph -> Q e. ( EE ` N ) )
7 linecgrand.7 
 |-  ( ( ph /\ ps ) -> A =/= B )
8 linecgrand.8 
 |-  ( ( ph /\ ps ) -> A Colinear <. B , C >. )
9 linecgrand.9 
 |-  ( ( ph /\ ps ) -> <. A , P >. Cgr <. A , Q >. )
10 linecgrand.10 
 |-  ( ( ph /\ ps ) -> <. B , P >. Cgr <. B , Q >. )
11 7 8 jca 
 |-  ( ( ph /\ ps ) -> ( A =/= B /\ A Colinear <. B , C >. ) )
12 9 10 jca 
 |-  ( ( ph /\ ps ) -> ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) )
13 linecgr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` 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 
 |-  ( ph -> ( ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) -> <. C , P >. Cgr <. C , Q >. ) )
15 14 adantr 
 |-  ( ( ph /\ ps ) -> ( ( ( 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 
 |-  ( ( ph /\ ps ) -> <. C , P >. Cgr <. C , Q >. )