Metamath Proof Explorer

Theorem cgrtrand

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

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

Proof

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