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

Theorem syl131anc 1278
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 1186 . 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 1265 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 983
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 985
This theorem is referenced by:  syl132anc  1283  syl231anc  1285  syl133anc  1288  initoeu2lem1  15902  estrres  16017  mulgdir  16776  3v3e3cycl2  25384  omndadd2d  28472  omndadd2rd  28473  submomnd  28474  omndmul2  28476  omndmul3  28477  ogrpinvOLD  28479  ogrpinv0le  28480  ogrpsub  28481  ogrpaddltbi  28483  ogrpaddltrd  28484  ogrpinv0lt  28487  isarchi3  28505  archirngz  28507  archiabllem1a  28509  archiabllem1b  28510  archiabllem2a  28512  archiabllem2c  28513  orngsqr  28569  ornglmulle  28570  orngrmulle  28571  ofldchr  28579  lineext  30842  brsegle2  30875  cvrcmp  32812  cvrcmp2  32813  atcvreq0  32843  cvlatexch3  32867  cvlcvr1  32868  cvlsupr2  32872  cvlsupr7  32877  atnlej1  32907  atnlej2  32908  cvrval3  32941  ltltncvr  32951  atcvrneN  32958  atcvrj2b  32960  atbtwnex  32976  3noncolr2  32977  3noncolr1N  32978  4noncolr3  32981  3dimlem2  32987  3dimlem3a  32988  3dimlem3  32989  3dimlem3OLDN  32990  3dimlem4a  32991  3dimlem4  32992  3dimlem4OLDN  32993  ps-1  33005  hlatexch4  33009  3atlem1  33011  3atlem2  33012  3atlem3  33013  3atlem4  33014  3atlem5  33015  3atlem6  33016  3atlem7  33017  2llnmat  33052  ps-2c  33056  lplnri3N  33083  lplnexllnN  33092  2llnmeqat  33099  4atlem0a  33121  4atlem0ae  33122  4atlem0be  33123  4atlem9  33131  4atlem10a  33132  4atlem10b  33133  4atlem10  33134  4atlem11a  33135  4atlem11  33137  4atlem12a  33138  dalemcnes  33178  dalempnes  33179  dalemqnet  33180  dalem1  33187  dalemdea  33190  dalem3  33192  dalem5  33195  dalem-cly  33199  dalem27  33227  dalem28  33228  dalem41  33241  dalem45  33245  dalem48  33248  lneq2at  33306  2lnat  33312  2llnma1  33315  2llnma3r  33316  2llnma2  33317  cdlemblem  33321  paddasslem2  33349  pmodl42N  33379  hlmod1i  33384  atmod1i1m  33386  atmod2i1  33389  atmod2i2  33390  atmod3i1  33392  llnexchb2lem  33396  dalawlem2  33400  dalawlem3  33401  dalawlem6  33404  dalawlem7  33405  dalawlem11  33409  dalawlem12  33410  pexmidlem3N  33500  lhpexle3lem  33539  lhpmcvr3  33553  lhp2at0  33560  lhpelim  33565  lhpmod2i2  33566  lhpmod6i1  33567  4atexlempns  33590  4atexlemunv  33594  4atexlemc  33597  4atexlemnclw  33598  4atexlemex2  33599  4atexlemex6  33602  4atex  33604  4atex3  33609  trljat1  33695  trljat2  33696  ltrnatlw  33712  trlval4  33717  cdlemc1  33720  cdlemc3  33722  cdlemc6  33725  cdlemd3  33729  cdlemd4  33730  cdlemd5  33731  cdlemd6  33732  cdlemd7  33733  cdleme00a  33738  cdleme0cp  33743  cdleme0cq  33744  cdleme0e  33746  cdleme02N  33751  cdleme0ex2N  33753  cdleme0moN  33754  cdleme1  33756  cdleme2  33757  cdleme3e  33761  cdleme3g  33763  cdleme3h  33764  cdleme4  33767  cdleme5  33769  cdleme7aa  33771  cdleme7c  33774  cdleme7d  33775  cdleme7e  33776  cdleme8  33779  cdleme9  33782  cdleme10  33783  cdleme16aN  33788  cdleme11a  33789  cdleme11c  33790  cdleme11dN  33791  cdleme11e  33792  cdleme11g  33794  cdleme11h  33795  cdleme11j  33796  cdleme11k  33797  cdleme12  33800  cdleme15a  33803  cdleme15b  33804  cdleme16b  33808  cdleme17c  33817  cdleme0nex  33819  cdleme18d  33824  cdlemednpq  33828  cdleme20zN  33830  cdleme20y  33831  cdleme20yOLD  33832  cdleme19a  33833  cdleme19d  33836  cdleme20aN  33839  cdleme20c  33841  cdleme20i  33847  cdleme20j  33848  cdleme21a  33855  cdleme21b  33856  cdleme21c  33857  cdleme21ct  33859  cdleme22cN  33872  cdleme22d  33873  cdleme22e  33874  cdleme22eALTN  33875  cdleme22f  33876  cdleme22f2  33877  cdleme22g  33878  cdleme23c  33881  cdleme41sn3a  33963  cdleme32le  33977  cdleme35b  33980  cdleme35c  33981  cdleme35d  33982  cdleme35e  33983  cdleme36a  33990  cdleme37m  33992  cdleme39a  33995  cdleme42a  34001  cdleme17d2  34025  cdlemeg46frv  34055  cdlemeg46rgv  34058  cdlemf1  34091  cdlemg2fv2  34130  cdlemg2l  34133  cdlemg2m  34134  cdlemg4d  34143  cdlemg4e  34144  cdlemg4f  34145  cdlemg4  34147  cdlemg6c  34150  cdlemg9a  34162  cdlemg10bALTN  34166  cdlemg12a  34173  cdlemg13  34182  cdlemg14f  34183  cdlemg14g  34184  cdlemg17i  34199  cdlemg17pq  34202  cdlemg19  34214  cdlemg21  34216  cdlemg27b  34226  cdlemg33c  34238  cdlemg33d  34239  trlcoabs2N  34252  cdlemg43  34260  cdlemg44b  34262  cdlemg44  34263  cdlemh1  34345  cdlemh2  34346  cdlemi1  34348  tendo0mul  34356  tendo0mulr  34357  cdlemk4  34364  cdlemk9  34369  cdlemk9bN  34370  cdlemk14  34384  cdlemkfid1N  34451  cdlemkid1  34452  cdlemk35s-id  34468  cdlemk39s-id  34470  cdlemk55a  34489  cdlemk55u  34496  cdlemk39u  34498  cdlemk19u  34500  cdlemk56  34501  cdleml8  34513  dia2dimlem1  34595  dia2dimlem2  34596  dia2dimlem3  34597  cdlemn10  34737  dihjust  34748  dihord1  34749  dihlsscpre  34765  dihvalcqpre  34766  dihglbcpreN  34831  dihmeetlem5  34839  dihmeetlem7N  34841  dihjatc1  34842  lincreslvec3  39619  isldepslvec2  39622
  Copyright terms: Public domain W3C validator