Metamath Proof Explorer

Theorem cgrextendand

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

Ref Expression
Hypotheses cgrextendand.1 
|- ( ph -> N e. NN )
cgrextendand.2 
|- ( ph -> A e. ( EE ` N ) )
cgrextendand.3 
|- ( ph -> B e. ( EE ` N ) )
cgrextendand.4 
|- ( ph -> C e. ( EE ` N ) )
cgrextendand.5 
|- ( ph -> D e. ( EE ` N ) )
cgrextendand.6 
|- ( ph -> E e. ( EE ` N ) )
cgrextendand.7 
|- ( ph -> F e. ( EE ` N ) )
cgrextendand.8 
|- ( ( ph /\ ps ) -> B Btwn <. A , C >. )
cgrextendand.9 
|- ( ( ph /\ ps ) -> E Btwn <. D , F >. )
cgrextendand.10 
|- ( ( ph /\ ps ) -> <. A , B >. Cgr <. D , E >. )
cgrextendand.11 
|- ( ( ph /\ ps ) -> <. B , C >. Cgr <. E , F >. )
Assertion cgrextendand 
|- ( ( ph /\ ps ) -> <. A , C >. Cgr <. D , F >. )

Proof

Step Hyp Ref Expression
1 cgrextendand.1 
 |-  ( ph -> N e. NN )
2 cgrextendand.2 
 |-  ( ph -> A e. ( EE ` N ) )
3 cgrextendand.3 
 |-  ( ph -> B e. ( EE ` N ) )
4 cgrextendand.4 
 |-  ( ph -> C e. ( EE ` N ) )
5 cgrextendand.5 
 |-  ( ph -> D e. ( EE ` N ) )
6 cgrextendand.6 
 |-  ( ph -> E e. ( EE ` N ) )
7 cgrextendand.7 
 |-  ( ph -> F e. ( EE ` N ) )
8 cgrextendand.8 
 |-  ( ( ph /\ ps ) -> B Btwn <. A , C >. )
9 cgrextendand.9 
 |-  ( ( ph /\ ps ) -> E Btwn <. D , F >. )
10 cgrextendand.10 
 |-  ( ( ph /\ ps ) -> <. A , B >. Cgr <. D , E >. )
11 cgrextendand.11 
 |-  ( ( ph /\ ps ) -> <. B , C >. Cgr <. E , F >. )
12 8 9 jca 
 |-  ( ( ph /\ ps ) -> ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) )
13 10 11 jca 
 |-  ( ( ph /\ ps ) -> ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) )
14 cgrextend 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` 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 
 |-  ( ph -> ( ( ( 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 
 |-  ( ( ph /\ ps ) -> ( ( ( 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 
 |-  ( ( ph /\ ps ) -> <. A , C >. Cgr <. D , F >. )