MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl131anc Structured version   Unicode version

Theorem syl131anc 1231
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
sylXanc.5  |-  ( ph  ->  et )
syl131anc.6  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  et )  ->  ze )
Assertion
Ref Expression
syl131anc  |-  ( ph  ->  ze )

Proof of Theorem syl131anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
52, 3, 43jca 1168 . 2  |-  ( ph  ->  ( ch  /\  th  /\  ta ) )
6 sylXanc.5 . 2  |-  ( ph  ->  et )
7 syl131anc.6 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  et )  ->  ze )
81, 5, 6, 7syl3anc 1218 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  syl132anc  1236  syl231anc  1238  syl133anc  1241  mulgdir  15652  3v3e3cycl2  23550  omndadd2d  26171  omndadd2rd  26172  omndmul2  26175  omndmul3  26176  ogrpinvOLD  26178  ogrpinv0le  26179  ogrpsub  26180  ogrpaddltbi  26182  ogrpaddltrd  26183  ogrpsublt  26185  ogrpinv0lt  26186  isarchi3  26204  archirngz  26206  archiabllem1a  26208  archiabllem1b  26209  archiabllem2a  26211  archiabllem2c  26212  ornglmulle  26273  orngrmulle  26274  lineext  28107  brsegle2  28140  lincreslvec3  31016  isldepslvec2  31019  cvrcmp  32928  cvrcmp2  32929  atcvreq0  32959  cvlatexch3  32983  cvlcvr1  32984  cvlsupr2  32988  cvlsupr7  32993  atnlej1  33023  atnlej2  33024  cvrval3  33057  ltltncvr  33067  atcvrneN  33074  atcvrj2b  33076  atbtwnex  33092  3noncolr2  33093  3noncolr1N  33094  4noncolr3  33097  3dimlem2  33103  3dimlem3a  33104  3dimlem3  33105  3dimlem3OLDN  33106  3dimlem4a  33107  3dimlem4  33108  3dimlem4OLDN  33109  ps-1  33121  hlatexch4  33125  3atlem1  33127  3atlem2  33128  3atlem3  33129  3atlem4  33130  3atlem5  33131  3atlem6  33132  3atlem7  33133  2llnmat  33168  ps-2c  33172  lplnri3N  33199  lplnexllnN  33208  2llnmeqat  33215  4atlem0a  33237  4atlem0ae  33238  4atlem0be  33239  4atlem9  33247  4atlem10a  33248  4atlem10b  33249  4atlem10  33250  4atlem11a  33251  4atlem11  33253  4atlem12a  33254  dalemcnes  33294  dalempnes  33295  dalemqnet  33296  dalem1  33303  dalemdea  33306  dalem3  33308  dalem5  33311  dalem-cly  33315  dalem27  33343  dalem28  33344  dalem41  33357  dalem45  33361  dalem48  33364  lneq2at  33422  2lnat  33428  2llnma1  33431  2llnma3r  33432  2llnma2  33433  cdlemblem  33437  paddasslem2  33465  pmodl42N  33495  hlmod1i  33500  atmod1i1m  33502  atmod2i1  33505  atmod2i2  33506  atmod3i1  33508  llnexchb2lem  33512  dalawlem2  33516  dalawlem3  33517  dalawlem6  33520  dalawlem7  33521  dalawlem11  33525  dalawlem12  33526  pexmidlem3N  33616  lhpexle3lem  33655  lhpmcvr3  33669  lhp2at0  33676  lhpelim  33681  lhpmod2i2  33682  lhpmod6i1  33683  4atexlempns  33706  4atexlemunv  33710  4atexlemc  33713  4atexlemnclw  33714  4atexlemex2  33715  4atexlemex6  33718  4atex  33720  4atex3  33725  trljat1  33810  trljat2  33811  ltrnatlw  33827  trlval4  33832  cdlemc1  33835  cdlemc3  33837  cdlemc6  33840  cdlemd3  33844  cdlemd4  33845  cdlemd5  33846  cdlemd6  33847  cdlemd7  33848  cdleme00a  33853  cdleme0cp  33858  cdleme0cq  33859  cdleme0e  33861  cdleme02N  33866  cdleme0ex2N  33868  cdleme0moN  33869  cdleme1  33871  cdleme2  33872  cdleme3e  33876  cdleme3g  33878  cdleme3h  33879  cdleme4  33882  cdleme5  33884  cdleme7aa  33886  cdleme7c  33889  cdleme7d  33890  cdleme7e  33891  cdleme8  33894  cdleme9  33897  cdleme10  33898  cdleme16aN  33903  cdleme11a  33904  cdleme11c  33905  cdleme11dN  33906  cdleme11e  33907  cdleme11g  33909  cdleme11h  33910  cdleme11j  33911  cdleme11k  33912  cdleme12  33915  cdleme15a  33918  cdleme15b  33919  cdleme16b  33923  cdleme17c  33932  cdleme0nex  33934  cdleme18d  33939  cdlemednpq  33943  cdleme20zN  33945  cdleme20y  33946  cdleme19a  33947  cdleme19d  33950  cdleme20aN  33953  cdleme20c  33955  cdleme20i  33961  cdleme20j  33962  cdleme21a  33969  cdleme21b  33970  cdleme21c  33971  cdleme21ct  33973  cdleme22cN  33986  cdleme22d  33987  cdleme22e  33988  cdleme22eALTN  33989  cdleme22f  33990  cdleme22f2  33991  cdleme22g  33992  cdleme23c  33995  cdleme41sn3a  34077  cdleme32le  34091  cdleme35b  34094  cdleme35c  34095  cdleme35d  34096  cdleme35e  34097  cdleme36a  34104  cdleme37m  34106  cdleme39a  34109  cdleme42a  34115  cdleme17d2  34139  cdlemeg46frv  34169  cdlemeg46rgv  34172  cdlemf1  34205  cdlemg2fv2  34244  cdlemg2l  34247  cdlemg2m  34248  cdlemg4d  34257  cdlemg4e  34258  cdlemg4f  34259  cdlemg4  34261  cdlemg6c  34264  cdlemg9a  34276  cdlemg10bALTN  34280  cdlemg12a  34287  cdlemg13  34296  cdlemg14f  34297  cdlemg14g  34298  cdlemg17i  34313  cdlemg17pq  34316  cdlemg19  34328  cdlemg21  34330  cdlemg27b  34340  cdlemg33c  34352  cdlemg33d  34353  trlcoabs2N  34366  cdlemg43  34374  cdlemg44b  34376  cdlemg44  34377  cdlemh1  34459  cdlemh2  34460  cdlemi1  34462  tendo0mul  34470  tendo0mulr  34471  cdlemk4  34478  cdlemk9  34483  cdlemk9bN  34484  cdlemk14  34498  cdlemkfid1N  34565  cdlemkid1  34566  cdlemk35s-id  34582  cdlemk39s-id  34584  cdlemk55a  34603  cdlemk55u  34610  cdlemk39u  34612  cdlemk19u  34614  cdlemk56  34615  cdleml8  34627  dia2dimlem1  34709  dia2dimlem2  34710  dia2dimlem3  34711  cdlemn10  34851  dihjust  34862  dihord1  34863  dihlsscpre  34879  dihvalcqpre  34880  dihglbcpreN  34945  dihmeetlem5  34953  dihmeetlem7N  34955  dihjatc1  34956
  Copyright terms: Public domain W3C validator