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

Theorem syl131anc 1281
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 1188 . 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 1268 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  syl132anc  1286  syl231anc  1288  syl133anc  1291  initoeu2lem1  15909  estrres  16024  mulgdir  16783  3v3e3cycl2  25392  omndadd2d  28471  omndadd2rd  28472  submomnd  28473  omndmul2  28475  omndmul3  28476  ogrpinvOLD  28478  ogrpinv0le  28479  ogrpsub  28480  ogrpaddltbi  28482  ogrpaddltrd  28483  ogrpinv0lt  28486  isarchi3  28504  archirngz  28506  archiabllem1a  28508  archiabllem1b  28509  archiabllem2a  28511  archiabllem2c  28512  orngsqr  28567  ornglmulle  28568  orngrmulle  28569  ofldchr  28577  lineext  30843  brsegle2  30876  cvrcmp  32849  cvrcmp2  32850  atcvreq0  32880  cvlatexch3  32904  cvlcvr1  32905  cvlsupr2  32909  cvlsupr7  32914  atnlej1  32944  atnlej2  32945  cvrval3  32978  ltltncvr  32988  atcvrneN  32995  atcvrj2b  32997  atbtwnex  33013  3noncolr2  33014  3noncolr1N  33015  4noncolr3  33018  3dimlem2  33024  3dimlem3a  33025  3dimlem3  33026  3dimlem3OLDN  33027  3dimlem4a  33028  3dimlem4  33029  3dimlem4OLDN  33030  ps-1  33042  hlatexch4  33046  3atlem1  33048  3atlem2  33049  3atlem3  33050  3atlem4  33051  3atlem5  33052  3atlem6  33053  3atlem7  33054  2llnmat  33089  ps-2c  33093  lplnri3N  33120  lplnexllnN  33129  2llnmeqat  33136  4atlem0a  33158  4atlem0ae  33159  4atlem0be  33160  4atlem9  33168  4atlem10a  33169  4atlem10b  33170  4atlem10  33171  4atlem11a  33172  4atlem11  33174  4atlem12a  33175  dalemcnes  33215  dalempnes  33216  dalemqnet  33217  dalem1  33224  dalemdea  33227  dalem3  33229  dalem5  33232  dalem-cly  33236  dalem27  33264  dalem28  33265  dalem41  33278  dalem45  33282  dalem48  33285  lneq2at  33343  2lnat  33349  2llnma1  33352  2llnma3r  33353  2llnma2  33354  cdlemblem  33358  paddasslem2  33386  pmodl42N  33416  hlmod1i  33421  atmod1i1m  33423  atmod2i1  33426  atmod2i2  33427  atmod3i1  33429  llnexchb2lem  33433  dalawlem2  33437  dalawlem3  33438  dalawlem6  33441  dalawlem7  33442  dalawlem11  33446  dalawlem12  33447  pexmidlem3N  33537  lhpexle3lem  33576  lhpmcvr3  33590  lhp2at0  33597  lhpelim  33602  lhpmod2i2  33603  lhpmod6i1  33604  4atexlempns  33627  4atexlemunv  33631  4atexlemc  33634  4atexlemnclw  33635  4atexlemex2  33636  4atexlemex6  33639  4atex  33641  4atex3  33646  trljat1  33732  trljat2  33733  ltrnatlw  33749  trlval4  33754  cdlemc1  33757  cdlemc3  33759  cdlemc6  33762  cdlemd3  33766  cdlemd4  33767  cdlemd5  33768  cdlemd6  33769  cdlemd7  33770  cdleme00a  33775  cdleme0cp  33780  cdleme0cq  33781  cdleme0e  33783  cdleme02N  33788  cdleme0ex2N  33790  cdleme0moN  33791  cdleme1  33793  cdleme2  33794  cdleme3e  33798  cdleme3g  33800  cdleme3h  33801  cdleme4  33804  cdleme5  33806  cdleme7aa  33808  cdleme7c  33811  cdleme7d  33812  cdleme7e  33813  cdleme8  33816  cdleme9  33819  cdleme10  33820  cdleme16aN  33825  cdleme11a  33826  cdleme11c  33827  cdleme11dN  33828  cdleme11e  33829  cdleme11g  33831  cdleme11h  33832  cdleme11j  33833  cdleme11k  33834  cdleme12  33837  cdleme15a  33840  cdleme15b  33841  cdleme16b  33845  cdleme17c  33854  cdleme0nex  33856  cdleme18d  33861  cdlemednpq  33865  cdleme20zN  33867  cdleme20y  33868  cdleme20yOLD  33869  cdleme19a  33870  cdleme19d  33873  cdleme20aN  33876  cdleme20c  33878  cdleme20i  33884  cdleme20j  33885  cdleme21a  33892  cdleme21b  33893  cdleme21c  33894  cdleme21ct  33896  cdleme22cN  33909  cdleme22d  33910  cdleme22e  33911  cdleme22eALTN  33912  cdleme22f  33913  cdleme22f2  33914  cdleme22g  33915  cdleme23c  33918  cdleme41sn3a  34000  cdleme32le  34014  cdleme35b  34017  cdleme35c  34018  cdleme35d  34019  cdleme35e  34020  cdleme36a  34027  cdleme37m  34029  cdleme39a  34032  cdleme42a  34038  cdleme17d2  34062  cdlemeg46frv  34092  cdlemeg46rgv  34095  cdlemf1  34128  cdlemg2fv2  34167  cdlemg2l  34170  cdlemg2m  34171  cdlemg4d  34180  cdlemg4e  34181  cdlemg4f  34182  cdlemg4  34184  cdlemg6c  34187  cdlemg9a  34199  cdlemg10bALTN  34203  cdlemg12a  34210  cdlemg13  34219  cdlemg14f  34220  cdlemg14g  34221  cdlemg17i  34236  cdlemg17pq  34239  cdlemg19  34251  cdlemg21  34253  cdlemg27b  34263  cdlemg33c  34275  cdlemg33d  34276  trlcoabs2N  34289  cdlemg43  34297  cdlemg44b  34299  cdlemg44  34300  cdlemh1  34382  cdlemh2  34383  cdlemi1  34385  tendo0mul  34393  tendo0mulr  34394  cdlemk4  34401  cdlemk9  34406  cdlemk9bN  34407  cdlemk14  34421  cdlemkfid1N  34488  cdlemkid1  34489  cdlemk35s-id  34505  cdlemk39s-id  34507  cdlemk55a  34526  cdlemk55u  34533  cdlemk39u  34535  cdlemk19u  34537  cdlemk56  34538  cdleml8  34550  dia2dimlem1  34632  dia2dimlem2  34633  dia2dimlem3  34634  cdlemn10  34774  dihjust  34785  dihord1  34786  dihlsscpre  34802  dihvalcqpre  34803  dihglbcpreN  34868  dihmeetlem5  34876  dihmeetlem7N  34878  dihjatc1  34879  lincreslvec3  40328  isldepslvec2  40331
  Copyright terms: Public domain W3C validator