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

Theorem syl131anc 1198
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 1135 . 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 1185 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  syl132anc  1203  syl231anc  1205  syl133anc  1208  mulgdir  14917  3v3e3cycl2  21653  ofldsqr  24242  ofldchr  24246  subofld  24247  lineext  26012  brsegle2  26045  cvrcmp  30083  cvrcmp2  30084  atcvreq0  30114  cvlatexch3  30138  cvlcvr1  30139  cvlsupr2  30143  cvlsupr7  30148  atnlej1  30178  atnlej2  30179  cvrval3  30212  ltltncvr  30222  atcvrneN  30229  atcvrj2b  30231  atbtwnex  30247  3noncolr2  30248  3noncolr1N  30249  4noncolr3  30252  3dimlem2  30258  3dimlem3a  30259  3dimlem3  30260  3dimlem3OLDN  30261  3dimlem4a  30262  3dimlem4  30263  3dimlem4OLDN  30264  ps-1  30276  hlatexch4  30280  3atlem1  30282  3atlem2  30283  3atlem3  30284  3atlem4  30285  3atlem5  30286  3atlem6  30287  3atlem7  30288  2llnmat  30323  ps-2c  30327  lplnri3N  30354  lplnexllnN  30363  2llnmeqat  30370  4atlem0a  30392  4atlem0ae  30393  4atlem0be  30394  4atlem9  30402  4atlem10a  30403  4atlem10b  30404  4atlem10  30405  4atlem11a  30406  4atlem11  30408  4atlem12a  30409  dalemcnes  30449  dalempnes  30450  dalemqnet  30451  dalem1  30458  dalemdea  30461  dalem3  30463  dalem5  30466  dalem-cly  30470  dalem27  30498  dalem28  30499  dalem41  30512  dalem45  30516  dalem48  30519  lneq2at  30577  2lnat  30583  2llnma1  30586  2llnma3r  30587  2llnma2  30588  cdlemblem  30592  paddasslem2  30620  pmodl42N  30650  hlmod1i  30655  atmod1i1m  30657  atmod2i1  30660  atmod2i2  30661  atmod3i1  30663  llnexchb2lem  30667  dalawlem2  30671  dalawlem3  30672  dalawlem6  30675  dalawlem7  30676  dalawlem11  30680  dalawlem12  30681  pexmidlem3N  30771  lhpexle3lem  30810  lhpmcvr3  30824  lhp2at0  30831  lhpelim  30836  lhpmod2i2  30837  lhpmod6i1  30838  4atexlempns  30861  4atexlemunv  30865  4atexlemc  30868  4atexlemnclw  30869  4atexlemex2  30870  4atexlemex6  30873  4atex  30875  4atex3  30880  trljat1  30965  trljat2  30966  ltrnatlw  30982  trlval4  30987  cdlemc1  30990  cdlemc3  30992  cdlemc6  30995  cdlemd3  30999  cdlemd4  31000  cdlemd5  31001  cdlemd6  31002  cdlemd7  31003  cdleme00a  31008  cdleme0cp  31013  cdleme0cq  31014  cdleme0e  31016  cdleme02N  31021  cdleme0ex2N  31023  cdleme0moN  31024  cdleme1  31026  cdleme2  31027  cdleme3e  31031  cdleme3g  31033  cdleme3h  31034  cdleme4  31037  cdleme5  31039  cdleme7aa  31041  cdleme7c  31044  cdleme7d  31045  cdleme7e  31046  cdleme8  31049  cdleme9  31052  cdleme10  31053  cdleme16aN  31058  cdleme11a  31059  cdleme11c  31060  cdleme11dN  31061  cdleme11e  31062  cdleme11g  31064  cdleme11h  31065  cdleme11j  31066  cdleme11k  31067  cdleme12  31070  cdleme15a  31073  cdleme15b  31074  cdleme16b  31078  cdleme17c  31087  cdleme0nex  31089  cdleme18d  31094  cdlemednpq  31098  cdleme20zN  31100  cdleme20y  31101  cdleme19a  31102  cdleme19d  31105  cdleme20aN  31108  cdleme20c  31110  cdleme20i  31116  cdleme20j  31117  cdleme21a  31124  cdleme21b  31125  cdleme21c  31126  cdleme21ct  31128  cdleme22cN  31141  cdleme22d  31142  cdleme22e  31143  cdleme22eALTN  31144  cdleme22f  31145  cdleme22f2  31146  cdleme22g  31147  cdleme23c  31150  cdleme41sn3a  31232  cdleme32le  31246  cdleme35b  31249  cdleme35c  31250  cdleme35d  31251  cdleme35e  31252  cdleme36a  31259  cdleme37m  31261  cdleme39a  31264  cdleme42a  31270  cdleme17d2  31294  cdlemeg46frv  31324  cdlemeg46rgv  31327  cdlemf1  31360  cdlemg2fv2  31399  cdlemg2l  31402  cdlemg2m  31403  cdlemg4d  31412  cdlemg4e  31413  cdlemg4f  31414  cdlemg4  31416  cdlemg6c  31419  cdlemg9a  31431  cdlemg10bALTN  31435  cdlemg12a  31442  cdlemg13  31451  cdlemg14f  31452  cdlemg14g  31453  cdlemg17i  31468  cdlemg17pq  31471  cdlemg19  31483  cdlemg21  31485  cdlemg27b  31495  cdlemg33c  31507  cdlemg33d  31508  trlcoabs2N  31521  cdlemg43  31529  cdlemg44b  31531  cdlemg44  31532  cdlemh1  31614  cdlemh2  31615  cdlemi1  31617  tendo0mul  31625  tendo0mulr  31626  cdlemk4  31633  cdlemk9  31638  cdlemk9bN  31639  cdlemk14  31653  cdlemkfid1N  31720  cdlemkid1  31721  cdlemk35s-id  31737  cdlemk39s-id  31739  cdlemk55a  31758  cdlemk55u  31765  cdlemk39u  31767  cdlemk19u  31769  cdlemk56  31770  cdleml8  31782  dia2dimlem1  31864  dia2dimlem2  31865  dia2dimlem3  31866  cdlemn10  32006  dihjust  32017  dihord1  32018  dihlsscpre  32034  dihvalcqpre  32035  dihglbcpreN  32100  dihmeetlem5  32108  dihmeetlem7N  32110  dihjatc1  32111
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator