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

Theorem syl131anc 1241
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 1176 . 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 1228 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 975
This theorem is referenced by:  syl132anc  1246  syl231anc  1248  syl133anc  1251  initoeu2lem1  15419  estrres  15534  mulgdir  16293  3v3e3cycl2  24790  omndadd2d  27850  omndadd2rd  27851  submomnd  27852  omndmul2  27854  omndmul3  27855  ogrpinvOLD  27857  ogrpinv0le  27858  ogrpsub  27859  ogrpaddltbi  27861  ogrpaddltrd  27862  ogrpinv0lt  27865  isarchi3  27883  archirngz  27885  archiabllem1a  27887  archiabllem1b  27888  archiabllem2a  27890  archiabllem2c  27891  orngsqr  27947  ornglmulle  27948  orngrmulle  27949  lineext  29888  brsegle2  29921  lincreslvec3  33185  isldepslvec2  33188  cvrcmp  35109  cvrcmp2  35110  atcvreq0  35140  cvlatexch3  35164  cvlcvr1  35165  cvlsupr2  35169  cvlsupr7  35174  atnlej1  35204  atnlej2  35205  cvrval3  35238  ltltncvr  35248  atcvrneN  35255  atcvrj2b  35257  atbtwnex  35273  3noncolr2  35274  3noncolr1N  35275  4noncolr3  35278  3dimlem2  35284  3dimlem3a  35285  3dimlem3  35286  3dimlem3OLDN  35287  3dimlem4a  35288  3dimlem4  35289  3dimlem4OLDN  35290  ps-1  35302  hlatexch4  35306  3atlem1  35308  3atlem2  35309  3atlem3  35310  3atlem4  35311  3atlem5  35312  3atlem6  35313  3atlem7  35314  2llnmat  35349  ps-2c  35353  lplnri3N  35380  lplnexllnN  35389  2llnmeqat  35396  4atlem0a  35418  4atlem0ae  35419  4atlem0be  35420  4atlem9  35428  4atlem10a  35429  4atlem10b  35430  4atlem10  35431  4atlem11a  35432  4atlem11  35434  4atlem12a  35435  dalemcnes  35475  dalempnes  35476  dalemqnet  35477  dalem1  35484  dalemdea  35487  dalem3  35489  dalem5  35492  dalem-cly  35496  dalem27  35524  dalem28  35525  dalem41  35538  dalem45  35542  dalem48  35545  lneq2at  35603  2lnat  35609  2llnma1  35612  2llnma3r  35613  2llnma2  35614  cdlemblem  35618  paddasslem2  35646  pmodl42N  35676  hlmod1i  35681  atmod1i1m  35683  atmod2i1  35686  atmod2i2  35687  atmod3i1  35689  llnexchb2lem  35693  dalawlem2  35697  dalawlem3  35698  dalawlem6  35701  dalawlem7  35702  dalawlem11  35706  dalawlem12  35707  pexmidlem3N  35797  lhpexle3lem  35836  lhpmcvr3  35850  lhp2at0  35857  lhpelim  35862  lhpmod2i2  35863  lhpmod6i1  35864  4atexlempns  35887  4atexlemunv  35891  4atexlemc  35894  4atexlemnclw  35895  4atexlemex2  35896  4atexlemex6  35899  4atex  35901  4atex3  35906  trljat1  35992  trljat2  35993  ltrnatlw  36009  trlval4  36014  cdlemc1  36017  cdlemc3  36019  cdlemc6  36022  cdlemd3  36026  cdlemd4  36027  cdlemd5  36028  cdlemd6  36029  cdlemd7  36030  cdleme00a  36035  cdleme0cp  36040  cdleme0cq  36041  cdleme0e  36043  cdleme02N  36048  cdleme0ex2N  36050  cdleme0moN  36051  cdleme1  36053  cdleme2  36054  cdleme3e  36058  cdleme3g  36060  cdleme3h  36061  cdleme4  36064  cdleme5  36066  cdleme7aa  36068  cdleme7c  36071  cdleme7d  36072  cdleme7e  36073  cdleme8  36076  cdleme9  36079  cdleme10  36080  cdleme16aN  36085  cdleme11a  36086  cdleme11c  36087  cdleme11dN  36088  cdleme11e  36089  cdleme11g  36091  cdleme11h  36092  cdleme11j  36093  cdleme11k  36094  cdleme12  36097  cdleme15a  36100  cdleme15b  36101  cdleme16b  36105  cdleme17c  36114  cdleme0nex  36116  cdleme18d  36121  cdlemednpq  36125  cdleme20zN  36127  cdleme20y  36128  cdleme20yOLD  36129  cdleme19a  36130  cdleme19d  36133  cdleme20aN  36136  cdleme20c  36138  cdleme20i  36144  cdleme20j  36145  cdleme21a  36152  cdleme21b  36153  cdleme21c  36154  cdleme21ct  36156  cdleme22cN  36169  cdleme22d  36170  cdleme22e  36171  cdleme22eALTN  36172  cdleme22f  36173  cdleme22f2  36174  cdleme22g  36175  cdleme23c  36178  cdleme41sn3a  36260  cdleme32le  36274  cdleme35b  36277  cdleme35c  36278  cdleme35d  36279  cdleme35e  36280  cdleme36a  36287  cdleme37m  36289  cdleme39a  36292  cdleme42a  36298  cdleme17d2  36322  cdlemeg46frv  36352  cdlemeg46rgv  36355  cdlemf1  36388  cdlemg2fv2  36427  cdlemg2l  36430  cdlemg2m  36431  cdlemg4d  36440  cdlemg4e  36441  cdlemg4f  36442  cdlemg4  36444  cdlemg6c  36447  cdlemg9a  36459  cdlemg10bALTN  36463  cdlemg12a  36470  cdlemg13  36479  cdlemg14f  36480  cdlemg14g  36481  cdlemg17i  36496  cdlemg17pq  36499  cdlemg19  36511  cdlemg21  36513  cdlemg27b  36523  cdlemg33c  36535  cdlemg33d  36536  trlcoabs2N  36549  cdlemg43  36557  cdlemg44b  36559  cdlemg44  36560  cdlemh1  36642  cdlemh2  36643  cdlemi1  36645  tendo0mul  36653  tendo0mulr  36654  cdlemk4  36661  cdlemk9  36666  cdlemk9bN  36667  cdlemk14  36681  cdlemkfid1N  36748  cdlemkid1  36749  cdlemk35s-id  36765  cdlemk39s-id  36767  cdlemk55a  36786  cdlemk55u  36793  cdlemk39u  36795  cdlemk19u  36797  cdlemk56  36798  cdleml8  36810  dia2dimlem1  36892  dia2dimlem2  36893  dia2dimlem3  36894  cdlemn10  37034  dihjust  37045  dihord1  37046  dihlsscpre  37062  dihvalcqpre  37063  dihglbcpreN  37128  dihmeetlem5  37136  dihmeetlem7N  37138  dihjatc1  37139
  Copyright terms: Public domain W3C validator