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

Theorem syl131anc 1243
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 1177 . 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 1230 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  syl132anc  1248  syl231anc  1250  syl133anc  1253  initoeu2lem1  15617  estrres  15732  mulgdir  16491  3v3e3cycl2  25081  omndadd2d  28150  omndadd2rd  28151  submomnd  28152  omndmul2  28154  omndmul3  28155  ogrpinvOLD  28157  ogrpinv0le  28158  ogrpsub  28159  ogrpaddltbi  28161  ogrpaddltrd  28162  ogrpinv0lt  28165  isarchi3  28183  archirngz  28185  archiabllem1a  28187  archiabllem1b  28188  archiabllem2a  28190  archiabllem2c  28191  orngsqr  28247  ornglmulle  28248  orngrmulle  28249  lineext  30414  brsegle2  30447  cvrcmp  32301  cvrcmp2  32302  atcvreq0  32332  cvlatexch3  32356  cvlcvr1  32357  cvlsupr2  32361  cvlsupr7  32366  atnlej1  32396  atnlej2  32397  cvrval3  32430  ltltncvr  32440  atcvrneN  32447  atcvrj2b  32449  atbtwnex  32465  3noncolr2  32466  3noncolr1N  32467  4noncolr3  32470  3dimlem2  32476  3dimlem3a  32477  3dimlem3  32478  3dimlem3OLDN  32479  3dimlem4a  32480  3dimlem4  32481  3dimlem4OLDN  32482  ps-1  32494  hlatexch4  32498  3atlem1  32500  3atlem2  32501  3atlem3  32502  3atlem4  32503  3atlem5  32504  3atlem6  32505  3atlem7  32506  2llnmat  32541  ps-2c  32545  lplnri3N  32572  lplnexllnN  32581  2llnmeqat  32588  4atlem0a  32610  4atlem0ae  32611  4atlem0be  32612  4atlem9  32620  4atlem10a  32621  4atlem10b  32622  4atlem10  32623  4atlem11a  32624  4atlem11  32626  4atlem12a  32627  dalemcnes  32667  dalempnes  32668  dalemqnet  32669  dalem1  32676  dalemdea  32679  dalem3  32681  dalem5  32684  dalem-cly  32688  dalem27  32716  dalem28  32717  dalem41  32730  dalem45  32734  dalem48  32737  lneq2at  32795  2lnat  32801  2llnma1  32804  2llnma3r  32805  2llnma2  32806  cdlemblem  32810  paddasslem2  32838  pmodl42N  32868  hlmod1i  32873  atmod1i1m  32875  atmod2i1  32878  atmod2i2  32879  atmod3i1  32881  llnexchb2lem  32885  dalawlem2  32889  dalawlem3  32890  dalawlem6  32893  dalawlem7  32894  dalawlem11  32898  dalawlem12  32899  pexmidlem3N  32989  lhpexle3lem  33028  lhpmcvr3  33042  lhp2at0  33049  lhpelim  33054  lhpmod2i2  33055  lhpmod6i1  33056  4atexlempns  33079  4atexlemunv  33083  4atexlemc  33086  4atexlemnclw  33087  4atexlemex2  33088  4atexlemex6  33091  4atex  33093  4atex3  33098  trljat1  33184  trljat2  33185  ltrnatlw  33201  trlval4  33206  cdlemc1  33209  cdlemc3  33211  cdlemc6  33214  cdlemd3  33218  cdlemd4  33219  cdlemd5  33220  cdlemd6  33221  cdlemd7  33222  cdleme00a  33227  cdleme0cp  33232  cdleme0cq  33233  cdleme0e  33235  cdleme02N  33240  cdleme0ex2N  33242  cdleme0moN  33243  cdleme1  33245  cdleme2  33246  cdleme3e  33250  cdleme3g  33252  cdleme3h  33253  cdleme4  33256  cdleme5  33258  cdleme7aa  33260  cdleme7c  33263  cdleme7d  33264  cdleme7e  33265  cdleme8  33268  cdleme9  33271  cdleme10  33272  cdleme16aN  33277  cdleme11a  33278  cdleme11c  33279  cdleme11dN  33280  cdleme11e  33281  cdleme11g  33283  cdleme11h  33284  cdleme11j  33285  cdleme11k  33286  cdleme12  33289  cdleme15a  33292  cdleme15b  33293  cdleme16b  33297  cdleme17c  33306  cdleme0nex  33308  cdleme18d  33313  cdlemednpq  33317  cdleme20zN  33319  cdleme20y  33320  cdleme20yOLD  33321  cdleme19a  33322  cdleme19d  33325  cdleme20aN  33328  cdleme20c  33330  cdleme20i  33336  cdleme20j  33337  cdleme21a  33344  cdleme21b  33345  cdleme21c  33346  cdleme21ct  33348  cdleme22cN  33361  cdleme22d  33362  cdleme22e  33363  cdleme22eALTN  33364  cdleme22f  33365  cdleme22f2  33366  cdleme22g  33367  cdleme23c  33370  cdleme41sn3a  33452  cdleme32le  33466  cdleme35b  33469  cdleme35c  33470  cdleme35d  33471  cdleme35e  33472  cdleme36a  33479  cdleme37m  33481  cdleme39a  33484  cdleme42a  33490  cdleme17d2  33514  cdlemeg46frv  33544  cdlemeg46rgv  33547  cdlemf1  33580  cdlemg2fv2  33619  cdlemg2l  33622  cdlemg2m  33623  cdlemg4d  33632  cdlemg4e  33633  cdlemg4f  33634  cdlemg4  33636  cdlemg6c  33639  cdlemg9a  33651  cdlemg10bALTN  33655  cdlemg12a  33662  cdlemg13  33671  cdlemg14f  33672  cdlemg14g  33673  cdlemg17i  33688  cdlemg17pq  33691  cdlemg19  33703  cdlemg21  33705  cdlemg27b  33715  cdlemg33c  33727  cdlemg33d  33728  trlcoabs2N  33741  cdlemg43  33749  cdlemg44b  33751  cdlemg44  33752  cdlemh1  33834  cdlemh2  33835  cdlemi1  33837  tendo0mul  33845  tendo0mulr  33846  cdlemk4  33853  cdlemk9  33858  cdlemk9bN  33859  cdlemk14  33873  cdlemkfid1N  33940  cdlemkid1  33941  cdlemk35s-id  33957  cdlemk39s-id  33959  cdlemk55a  33978  cdlemk55u  33985  cdlemk39u  33987  cdlemk19u  33989  cdlemk56  33990  cdleml8  34002  dia2dimlem1  34084  dia2dimlem2  34085  dia2dimlem3  34086  cdlemn10  34226  dihjust  34237  dihord1  34238  dihlsscpre  34254  dihvalcqpre  34255  dihglbcpreN  34320  dihmeetlem5  34328  dihmeetlem7N  34330  dihjatc1  34331  lincreslvec3  38594  isldepslvec2  38597
  Copyright terms: Public domain W3C validator