Theorem syl122anc 1335

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	|- ( ph -> ps )
syl12anc.2	|- ( ph -> ch )
syl12anc.3	|- ( ph -> th )
syl22anc.4	|- ( ph -> ta )
syl23anc.5	|- ( ph -> et )
syl122anc.6	|- ( ( ps /\ ( ch /\ th ) /\ ( ta /\ et ) ) -> ze )

Assertion

Ref	Expression
syl122anc	|- ( ph -> ze )

Proof of Theorem syl122anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 |- ( ph -> ps )
2		syl12anc.2	. 2 |- ( ph -> ch )
3		syl12anc.3	. 2 |- ( ph -> th )
4		syl22anc.4	. . 3 |- ( ph -> ta )
5		syl23anc.5	. . 3 |- ( ph -> et )
6	4, 5	jca 554	. 2 |- ( ph -> ( ta /\ et ) )
7		syl122anc.6	. 2 |- ( ( ps /\ ( ch /\ th ) /\ ( ta /\ et ) ) -> ze )
8	1, 2, 3, 6, 7	syl121anc 1331	1 |- ( ph -> ze )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  divdiv32d  10826  divcan5d  10827  divcan7d  10829  divdiv1d  10832  divdiv2d  10833  seqcoll  13248  cau3lem  14094  eqsqrtd  14107  isercolllem2  14396  isercoll  14398  summolem2a  14446  divrcnv  14584  prodmolem2a  14664  prmind2  15398  divnumden  15456  pceulem  15550  pcqmul  15558  pcqdiv  15562  pcexp  15564  pcaddlem  15592  pcbc  15604  prmodvdslcmf  15751  latledi  17089  latjjdi  17103  latjjdir  17104  sylow1lem1  18013  sylow1lem5  18017  efgred2  18166  abladdsub4  18219  ablpnpcan  18225  ghmplusg  18249  frgpnabllem2  18277  isabvd  18820  lmodvs1  18891  lspsolvlem  19142  evlslem1  19515  frgpcyg  19922  ip2di  19986  mdetuni0  20427  cpmadugsumlemB  20679  elptr2  21377  blss2ps  22208  blss2  22209  blssps  22229  blss  22230  xmeter  22238  metdcnlem  22639  lebnumii  22765  minveclem2  23197  pjthlem1  23208  volfiniun  23315  dvfsumrlimge0  23793  lgsdi  25059  ax5seglem3  25811  ax5seglem6  25814  axcontlem8  25851  eengtrkg  25865  vacn  27549  minvecolem2  27731  minvecolem4  27736  disjabrex  29395  disjabrexf  29396  slmdvs1  29773  slmd0vs  29777  orngsqr  29804  ornglmulle  29805  orngrmulle  29806  orngmullt  29809  suborng  29815  madjusmdetlem1  29893  cgrcomand  32098  cgrcomr  32104  cgrcomland  32106  cgrcomrand  32107  cgrtriv  32109  cgrid2  32110  ofscom  32114  cgrextend  32115  segconeq  32117  btwntriv2  32119  btwnexch3and  32128  btwnouttr2  32129  btwnouttr  32131  btwnexch  32132  btwnexchand  32133  btwndiff  32134  ifscgr  32151  cgrsub  32152  cgrxfr  32162  lineext  32183  endofsegid  32192  btwnconn1lem2  32195  btwnconn1lem3  32196  btwnconn1lem4  32197  btwnconn1lem5  32198  btwnconn1lem7  32200  btwnconn1lem8  32201  btwnconn1lem10  32203  btwnconn1lem11  32204  btwnconn1lem13  32206  btwnconn1lem14  32207  btwnconn3  32210  midofsegid  32211  segcon2  32212  brsegle2  32216  seglecgr12im  32217  seglecgr12  32218  seglerflx  32219  seglemin  32220  segletr  32221  btwnsegle  32224  colinbtwnle  32225  btwnoutside  32232  broutsideof3  32233  outsideoftr  32236  outsideofeq  32237  outsidele  32239  lineunray  32254  lineelsb2  32255  lfladdcl  34358  lshpkrlem4  34400  latmmdiN  34521  latmmdir  34522  hlatj4  34660  4atlem4b  34886  4atlem11  34895  4atlem12  34898  dalem2  34947  dalem-cly  34957  dalem10  34959  dalem23  34982  dalem38  34996  dalem44  35002  dalem55  35013  cdlema1N  35077  paddclN  35128  pmapjoin  35138  dalawlem3  35159  dalawlem5  35161  dalawlem7  35163  dalawlem8  35164  dalawlem11  35167  dalawlem12  35168  lhpexle3lem  35297  4atexlemc  35355  trlnidat  35460  arglem1N  35477  cdlemd9  35493  cdleme0moN  35512  cdleme11c  35548  cdleme11h  35553  cdleme11  35557  cdleme16c  35567  cdleme16f  35570  cdlemeda  35585  cdleme20l2  35609  cdlemefs32sn1aw  35702  cdleme43fsv1snlem  35708  cdleme41sn3a  35721  cdleme32fva  35725  cdleme32b  35730  cdleme32c  35731  cdleme32e  35733  cdleme40m  35755  cdleme40n  35756  cdleme42e  35767  cdleme48d  35823  cdlemf2  35850  cdlemf  35851  cdlemg2fv2  35888  cdlemg7fvbwN  35895  cdlemg7fvN  35912  cdlemg9a  35920  cdlemg9b  35921  cdlemg10a  35928  cdlemg12b  35932  cdlemg17b  35950  cdlemg31d  35988  cdlemg33b0  35989  cdlemg33a  35994  ltrnco  36007  ltrncom  36026  cdlemh  36105  cdlemk3  36121  cdlemk12  36138  cdlemk12u  36160  cdlemkfid1N  36209  cdlemk51  36241  cdlemk54  36246  cdlemk43N  36251  cdlemk35u  36252  cdlemk55u1  36253  cdlemk39u1  36255  cdlemk19u1  36257  dia2dimlem10  36362  dvhgrp  36396  dvh0g  36400  cdlemm10N  36407  diblsmopel  36460  cdlemn4  36487  cdlemn6  36491  cdlemn7  36492  dihordlem7  36503  dihord1  36507  dihord2pre  36514  dihvalcqat  36528  dihopelvalcpre  36537  dihord5apre  36551  dihord  36553  dih1  36575  dihglbcpreN  36589  dihjatc1  36600  dihmeetlem13N  36608  dihmeetALTN  36616  dihjatcclem1  36707  baerlem3lem1  36996  pellfundex  37450  rmxypairf1o  37476  rmxycomplete  37482  rmxyneg  37485  rmxyadd  37486  rmxy1  37487  rmxy0  37488  jm2.22  37562  proot1mul  37777  deg1mhm  37785  stoweidlem7  40224  stoweidlem36  40253