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

Theorem syl131anc 1195
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 1132 . 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 1182 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl132anc  1200  syl231anc  1202  syl133anc  1205  mulgdir  14592  lineext  24699  brsegle2  24732  cvrcmp  29473  cvrcmp2  29474  atcvreq0  29504  cvlatexch3  29528  cvlcvr1  29529  cvlsupr2  29533  cvlsupr7  29538  atnlej1  29568  atnlej2  29569  cvrval3  29602  ltltncvr  29612  atcvrneN  29619  atcvrj2b  29621  atbtwnex  29637  3noncolr2  29638  3noncolr1N  29639  4noncolr3  29642  3dimlem2  29648  3dimlem3a  29649  3dimlem3  29650  3dimlem3OLDN  29651  3dimlem4a  29652  3dimlem4  29653  3dimlem4OLDN  29654  ps-1  29666  hlatexch4  29670  3atlem1  29672  3atlem2  29673  3atlem3  29674  3atlem4  29675  3atlem5  29676  3atlem6  29677  3atlem7  29678  2llnmat  29713  ps-2c  29717  lplnri3N  29744  lplnexllnN  29753  2llnmeqat  29760  4atlem0a  29782  4atlem0ae  29783  4atlem0be  29784  4atlem9  29792  4atlem10a  29793  4atlem10b  29794  4atlem10  29795  4atlem11a  29796  4atlem11  29798  4atlem12a  29799  dalemcnes  29839  dalempnes  29840  dalemqnet  29841  dalem1  29848  dalemdea  29851  dalem3  29853  dalem5  29856  dalem-cly  29860  dalem27  29888  dalem28  29889  dalem41  29902  dalem45  29906  dalem48  29909  lneq2at  29967  2lnat  29973  2llnma1  29976  2llnma3r  29977  2llnma2  29978  cdlemblem  29982  paddasslem2  30010  pmodl42N  30040  hlmod1i  30045  atmod1i1m  30047  atmod2i1  30050  atmod2i2  30051  atmod3i1  30053  llnexchb2lem  30057  dalawlem2  30061  dalawlem3  30062  dalawlem6  30065  dalawlem7  30066  dalawlem11  30070  dalawlem12  30071  pexmidlem3N  30161  lhpexle3lem  30200  lhpmcvr3  30214  lhp2at0  30221  lhpelim  30226  lhpmod2i2  30227  lhpmod6i1  30228  4atexlempns  30251  4atexlemunv  30255  4atexlemc  30258  4atexlemnclw  30259  4atexlemex2  30260  4atexlemex6  30263  4atex  30265  4atex3  30270  trljat1  30355  trljat2  30356  ltrnatlw  30372  trlval4  30377  cdlemc1  30380  cdlemc3  30382  cdlemc6  30385  cdlemd3  30389  cdlemd4  30390  cdlemd5  30391  cdlemd6  30392  cdlemd7  30393  cdleme00a  30398  cdleme0cp  30403  cdleme0cq  30404  cdleme0e  30406  cdleme02N  30411  cdleme0ex2N  30413  cdleme0moN  30414  cdleme1  30416  cdleme2  30417  cdleme3e  30421  cdleme3g  30423  cdleme3h  30424  cdleme4  30427  cdleme5  30429  cdleme7aa  30431  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme8  30439  cdleme9  30442  cdleme10  30443  cdleme16aN  30448  cdleme11a  30449  cdleme11c  30450  cdleme11dN  30451  cdleme11e  30452  cdleme11g  30454  cdleme11h  30455  cdleme11j  30456  cdleme11k  30457  cdleme12  30460  cdleme15a  30463  cdleme15b  30464  cdleme16b  30468  cdleme17c  30477  cdleme0nex  30479  cdleme18d  30484  cdlemednpq  30488  cdleme20zN  30490  cdleme20y  30491  cdleme19a  30492  cdleme19d  30495  cdleme20aN  30498  cdleme20c  30500  cdleme20i  30506  cdleme20j  30507  cdleme21a  30514  cdleme21b  30515  cdleme21c  30516  cdleme21ct  30518  cdleme22cN  30531  cdleme22d  30532  cdleme22e  30533  cdleme22eALTN  30534  cdleme22f  30535  cdleme22f2  30536  cdleme22g  30537  cdleme23c  30540  cdleme41sn3a  30622  cdleme32le  30636  cdleme35b  30639  cdleme35c  30640  cdleme35d  30641  cdleme35e  30642  cdleme36a  30649  cdleme37m  30651  cdleme39a  30654  cdleme42a  30660  cdleme17d2  30684  cdlemeg46frv  30714  cdlemeg46rgv  30717  cdlemf1  30750  cdlemg2fv2  30789  cdlemg2l  30792  cdlemg2m  30793  cdlemg4d  30802  cdlemg4e  30803  cdlemg4f  30804  cdlemg4  30806  cdlemg6c  30809  cdlemg9a  30821  cdlemg10bALTN  30825  cdlemg12a  30832  cdlemg13  30841  cdlemg14f  30842  cdlemg14g  30843  cdlemg17i  30858  cdlemg17pq  30861  cdlemg19  30873  cdlemg21  30875  cdlemg27b  30885  cdlemg33c  30897  cdlemg33d  30898  trlcoabs2N  30911  cdlemg43  30919  cdlemg44b  30921  cdlemg44  30922  cdlemh1  31004  cdlemh2  31005  cdlemi1  31007  tendo0mul  31015  tendo0mulr  31016  cdlemk4  31023  cdlemk9  31028  cdlemk9bN  31029  cdlemk14  31043  cdlemkfid1N  31110  cdlemkid1  31111  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk55a  31148  cdlemk55u  31155  cdlemk39u  31157  cdlemk19u  31159  cdlemk56  31160  cdleml8  31172  dia2dimlem1  31254  dia2dimlem2  31255  dia2dimlem3  31256  cdlemn10  31396  dihjust  31407  dihord1  31408  dihlsscpre  31424  dihvalcqpre  31425  dihglbcpreN  31490  dihmeetlem5  31498  dihmeetlem7N  31500  dihjatc1  31501
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator