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  14608  lineext  24771  brsegle2  24804  3v3e3cycl2  28410  cvrcmp  30095  cvrcmp2  30096  atcvreq0  30126  cvlatexch3  30150  cvlcvr1  30151  cvlsupr2  30155  cvlsupr7  30160  atnlej1  30190  atnlej2  30191  cvrval3  30224  ltltncvr  30234  atcvrneN  30241  atcvrj2b  30243  atbtwnex  30259  3noncolr2  30260  3noncolr1N  30261  4noncolr3  30264  3dimlem2  30270  3dimlem3a  30271  3dimlem3  30272  3dimlem3OLDN  30273  3dimlem4a  30274  3dimlem4  30275  3dimlem4OLDN  30276  ps-1  30288  hlatexch4  30292  3atlem1  30294  3atlem2  30295  3atlem3  30296  3atlem4  30297  3atlem5  30298  3atlem6  30299  3atlem7  30300  2llnmat  30335  ps-2c  30339  lplnri3N  30366  lplnexllnN  30375  2llnmeqat  30382  4atlem0a  30404  4atlem0ae  30405  4atlem0be  30406  4atlem9  30414  4atlem10a  30415  4atlem10b  30416  4atlem10  30417  4atlem11a  30418  4atlem11  30420  4atlem12a  30421  dalemcnes  30461  dalempnes  30462  dalemqnet  30463  dalem1  30470  dalemdea  30473  dalem3  30475  dalem5  30478  dalem-cly  30482  dalem27  30510  dalem28  30511  dalem41  30524  dalem45  30528  dalem48  30531  lneq2at  30589  2lnat  30595  2llnma1  30598  2llnma3r  30599  2llnma2  30600  cdlemblem  30604  paddasslem2  30632  pmodl42N  30662  hlmod1i  30667  atmod1i1m  30669  atmod2i1  30672  atmod2i2  30673  atmod3i1  30675  llnexchb2lem  30679  dalawlem2  30683  dalawlem3  30684  dalawlem6  30687  dalawlem7  30688  dalawlem11  30692  dalawlem12  30693  pexmidlem3N  30783  lhpexle3lem  30822  lhpmcvr3  30836  lhp2at0  30843  lhpelim  30848  lhpmod2i2  30849  lhpmod6i1  30850  4atexlempns  30873  4atexlemunv  30877  4atexlemc  30880  4atexlemnclw  30881  4atexlemex2  30882  4atexlemex6  30885  4atex  30887  4atex3  30892  trljat1  30977  trljat2  30978  ltrnatlw  30994  trlval4  30999  cdlemc1  31002  cdlemc3  31004  cdlemc6  31007  cdlemd3  31011  cdlemd4  31012  cdlemd5  31013  cdlemd6  31014  cdlemd7  31015  cdleme00a  31020  cdleme0cp  31025  cdleme0cq  31026  cdleme0e  31028  cdleme02N  31033  cdleme0ex2N  31035  cdleme0moN  31036  cdleme1  31038  cdleme2  31039  cdleme3e  31043  cdleme3g  31045  cdleme3h  31046  cdleme4  31049  cdleme5  31051  cdleme7aa  31053  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme8  31061  cdleme9  31064  cdleme10  31065  cdleme16aN  31070  cdleme11a  31071  cdleme11c  31072  cdleme11dN  31073  cdleme11e  31074  cdleme11g  31076  cdleme11h  31077  cdleme11j  31078  cdleme11k  31079  cdleme12  31082  cdleme15a  31085  cdleme15b  31086  cdleme16b  31090  cdleme17c  31099  cdleme0nex  31101  cdleme18d  31106  cdlemednpq  31110  cdleme20zN  31112  cdleme20y  31113  cdleme19a  31114  cdleme19d  31117  cdleme20aN  31120  cdleme20c  31122  cdleme20i  31128  cdleme20j  31129  cdleme21a  31136  cdleme21b  31137  cdleme21c  31138  cdleme21ct  31140  cdleme22cN  31153  cdleme22d  31154  cdleme22e  31155  cdleme22eALTN  31156  cdleme22f  31157  cdleme22f2  31158  cdleme22g  31159  cdleme23c  31162  cdleme41sn3a  31244  cdleme32le  31258  cdleme35b  31261  cdleme35c  31262  cdleme35d  31263  cdleme35e  31264  cdleme36a  31271  cdleme37m  31273  cdleme39a  31276  cdleme42a  31282  cdleme17d2  31306  cdlemeg46frv  31336  cdlemeg46rgv  31339  cdlemf1  31372  cdlemg2fv2  31411  cdlemg2l  31414  cdlemg2m  31415  cdlemg4d  31424  cdlemg4e  31425  cdlemg4f  31426  cdlemg4  31428  cdlemg6c  31431  cdlemg9a  31443  cdlemg10bALTN  31447  cdlemg12a  31454  cdlemg13  31463  cdlemg14f  31464  cdlemg14g  31465  cdlemg17i  31480  cdlemg17pq  31483  cdlemg19  31495  cdlemg21  31497  cdlemg27b  31507  cdlemg33c  31519  cdlemg33d  31520  trlcoabs2N  31533  cdlemg43  31541  cdlemg44b  31543  cdlemg44  31544  cdlemh1  31626  cdlemh2  31627  cdlemi1  31629  tendo0mul  31637  tendo0mulr  31638  cdlemk4  31645  cdlemk9  31650  cdlemk9bN  31651  cdlemk14  31665  cdlemkfid1N  31732  cdlemkid1  31733  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk55a  31770  cdlemk55u  31777  cdlemk39u  31779  cdlemk19u  31781  cdlemk56  31782  cdleml8  31794  dia2dimlem1  31876  dia2dimlem2  31877  dia2dimlem3  31878  cdlemn10  32018  dihjust  32029  dihord1  32030  dihlsscpre  32046  dihvalcqpre  32047  dihglbcpreN  32112  dihmeetlem5  32120  dihmeetlem7N  32122  dihjatc1  32123
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