Theorem syl131anc 1339

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 )
syl131anc.6	|- ( ( ps /\ ( ch /\ th /\ ta ) /\ et ) -> ze )

Assertion

Ref	Expression
syl131anc	|- ( ph -> ze )

Proof of Theorem syl131anc

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

Syntax hints:   -> wi 4   /\ 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:  syl132anc  1344  syl231anc  1346  syl133anc  1349  initoeu2lem1  16664  estrres  16779  mulgdir  17573  2pthfrgr  27148  omndadd2d  29708  omndadd2rd  29709  submomnd  29710  omndmul2  29712  omndmul3  29713  ogrpinvOLD  29715  ogrpinv0le  29716  ogrpsub  29717  ogrpaddltbi  29719  ogrpaddltrd  29720  ogrpinv0lt  29723  isarchi3  29741  archirngz  29743  archiabllem1a  29745  archiabllem1b  29746  archiabllem2a  29748  archiabllem2c  29749  orngsqr  29804  ornglmulle  29805  orngrmulle  29806  ofldchr  29814  lineext  32183  brsegle2  32216  cvrcmp  34570  cvrcmp2  34571  atcvreq0  34601  cvlatexch3  34625  cvlcvr1  34626  cvlsupr2  34630  cvlsupr7  34635  atnlej1  34665  atnlej2  34666  cvrval3  34699  ltltncvr  34709  atcvrneN  34716  atcvrj2b  34718  atbtwnex  34734  3noncolr2  34735  3noncolr1N  34736  4noncolr3  34739  3dimlem2  34745  3dimlem3a  34746  3dimlem3  34747  3dimlem3OLDN  34748  3dimlem4a  34749  3dimlem4  34750  3dimlem4OLDN  34751  ps-1  34763  hlatexch4  34767  3atlem1  34769  3atlem2  34770  3atlem3  34771  3atlem4  34772  3atlem5  34773  3atlem6  34774  3atlem7  34775  2llnmat  34810  ps-2c  34814  lplnri3N  34841  lplnexllnN  34850  2llnmeqat  34857  4atlem0a  34879  4atlem0ae  34880  4atlem0be  34881  4atlem9  34889  4atlem10a  34890  4atlem10b  34891  4atlem10  34892  4atlem11a  34893  4atlem11  34895  4atlem12a  34896  dalemcnes  34936  dalempnes  34937  dalemqnet  34938  dalem1  34945  dalemdea  34948  dalem3  34950  dalem5  34953  dalem-cly  34957  dalem27  34985  dalem28  34986  dalem41  34999  dalem45  35003  dalem48  35006  lneq2at  35064  2lnat  35070  2llnma1  35073  2llnma3r  35074  2llnma2  35075  cdlemblem  35079  paddasslem2  35107  pmodl42N  35137  hlmod1i  35142  atmod1i1m  35144  atmod2i1  35147  atmod2i2  35148  atmod3i1  35150  llnexchb2lem  35154  dalawlem2  35158  dalawlem3  35159  dalawlem6  35162  dalawlem7  35163  dalawlem11  35167  dalawlem12  35168  pexmidlem3N  35258  lhpexle3lem  35297  lhpmcvr3  35311  lhp2at0  35318  lhpelim  35323  lhpmod2i2  35324  lhpmod6i1  35325  4atexlempns  35348  4atexlemunv  35352  4atexlemc  35355  4atexlemnclw  35356  4atexlemex2  35357  4atexlemex6  35360  4atex  35362  4atex3  35367  trljat1  35453  trljat2  35454  ltrnatlw  35470  trlval4  35475  cdlemc1  35478  cdlemc3  35480  cdlemc6  35483  cdlemd3  35487  cdlemd4  35488  cdlemd5  35489  cdlemd6  35490  cdlemd7  35491  cdleme00a  35496  cdleme0cp  35501  cdleme0cq  35502  cdleme0e  35504  cdleme02N  35509  cdleme0ex2N  35511  cdleme0moN  35512  cdleme1  35514  cdleme2  35515  cdleme3e  35519  cdleme3g  35521  cdleme3h  35522  cdleme4  35525  cdleme5  35527  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme8  35537  cdleme9  35540  cdleme10  35541  cdleme16aN  35546  cdleme11a  35547  cdleme11c  35548  cdleme11dN  35549  cdleme11e  35550  cdleme11g  35552  cdleme11h  35553  cdleme11j  35554  cdleme11k  35555  cdleme12  35558  cdleme15a  35561  cdleme15b  35562  cdleme16b  35566  cdleme17c  35575  cdleme0nex  35577  cdleme18d  35582  cdlemednpq  35586  cdleme20zN  35588  cdleme20y  35589  cdleme20yOLD  35590  cdleme19a  35591  cdleme19d  35594  cdleme20aN  35597  cdleme20c  35599  cdleme20i  35605  cdleme20j  35606  cdleme21a  35613  cdleme21b  35614  cdleme21c  35615  cdleme21ct  35617  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f  35634  cdleme22f2  35635  cdleme22g  35636  cdleme23c  35639  cdleme41sn3a  35721  cdleme32le  35735  cdleme35b  35738  cdleme35c  35739  cdleme35d  35740  cdleme35e  35741  cdleme36a  35748  cdleme37m  35750  cdleme39a  35753  cdleme42a  35759  cdleme17d2  35783  cdlemeg46frv  35813  cdlemeg46rgv  35816  cdlemf1  35849  cdlemg2fv2  35888  cdlemg2l  35891  cdlemg2m  35892  cdlemg4d  35901  cdlemg4e  35902  cdlemg4f  35903  cdlemg4  35905  cdlemg6c  35908  cdlemg9a  35920  cdlemg10bALTN  35924  cdlemg12a  35931  cdlemg13  35940  cdlemg14f  35941  cdlemg14g  35942  cdlemg17i  35957  cdlemg17pq  35960  cdlemg19  35972  cdlemg21  35974  cdlemg27b  35984  cdlemg33c  35996  cdlemg33d  35997  trlcoabs2N  36010  cdlemg43  36018  cdlemg44b  36020  cdlemg44  36021  cdlemh1  36103  cdlemh2  36104  cdlemi1  36106  tendo0mul  36114  tendo0mulr  36115  cdlemk4  36122  cdlemk9  36127  cdlemk9bN  36128  cdlemk14  36142  cdlemkfid1N  36209  cdlemkid1  36210  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk55a  36247  cdlemk55u  36254  cdlemk39u  36256  cdlemk19u  36258  cdlemk56  36259  cdleml8  36271  dia2dimlem1  36353  dia2dimlem2  36354  dia2dimlem3  36355  cdlemn10  36495  dihjust  36506  dihord1  36507  dihlsscpre  36523  dihvalcqpre  36524  dihglbcpreN  36589  dihmeetlem5  36597  dihmeetlem7N  36599  dihjatc1  36600  lincreslvec3  42271  isldepslvec2  42274