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  mulgdir  15977  3v3e3cycl2  24368  omndadd2d  27388  omndadd2rd  27389  omndmul2  27392  omndmul3  27393  ogrpinvOLD  27395  ogrpinv0le  27396  ogrpsub  27397  ogrpaddltbi  27399  ogrpaddltrd  27400  ogrpsublt  27402  ogrpinv0lt  27403  isarchi3  27421  archirngz  27423  archiabllem1a  27425  archiabllem1b  27426  archiabllem2a  27428  archiabllem2c  27429  ornglmulle  27486  orngrmulle  27487  lineext  29331  brsegle2  29364  lincreslvec3  32182  isldepslvec2  32185  cvrcmp  34098  cvrcmp2  34099  atcvreq0  34129  cvlatexch3  34153  cvlcvr1  34154  cvlsupr2  34158  cvlsupr7  34163  atnlej1  34193  atnlej2  34194  cvrval3  34227  ltltncvr  34237  atcvrneN  34244  atcvrj2b  34246  atbtwnex  34262  3noncolr2  34263  3noncolr1N  34264  4noncolr3  34267  3dimlem2  34273  3dimlem3a  34274  3dimlem3  34275  3dimlem3OLDN  34276  3dimlem4a  34277  3dimlem4  34278  3dimlem4OLDN  34279  ps-1  34291  hlatexch4  34295  3atlem1  34297  3atlem2  34298  3atlem3  34299  3atlem4  34300  3atlem5  34301  3atlem6  34302  3atlem7  34303  2llnmat  34338  ps-2c  34342  lplnri3N  34369  lplnexllnN  34378  2llnmeqat  34385  4atlem0a  34407  4atlem0ae  34408  4atlem0be  34409  4atlem9  34417  4atlem10a  34418  4atlem10b  34419  4atlem10  34420  4atlem11a  34421  4atlem11  34423  4atlem12a  34424  dalemcnes  34464  dalempnes  34465  dalemqnet  34466  dalem1  34473  dalemdea  34476  dalem3  34478  dalem5  34481  dalem-cly  34485  dalem27  34513  dalem28  34514  dalem41  34527  dalem45  34531  dalem48  34534  lneq2at  34592  2lnat  34598  2llnma1  34601  2llnma3r  34602  2llnma2  34603  cdlemblem  34607  paddasslem2  34635  pmodl42N  34665  hlmod1i  34670  atmod1i1m  34672  atmod2i1  34675  atmod2i2  34676  atmod3i1  34678  llnexchb2lem  34682  dalawlem2  34686  dalawlem3  34687  dalawlem6  34690  dalawlem7  34691  dalawlem11  34695  dalawlem12  34696  pexmidlem3N  34786  lhpexle3lem  34825  lhpmcvr3  34839  lhp2at0  34846  lhpelim  34851  lhpmod2i2  34852  lhpmod6i1  34853  4atexlempns  34876  4atexlemunv  34880  4atexlemc  34883  4atexlemnclw  34884  4atexlemex2  34885  4atexlemex6  34888  4atex  34890  4atex3  34895  trljat1  34980  trljat2  34981  ltrnatlw  34997  trlval4  35002  cdlemc1  35005  cdlemc3  35007  cdlemc6  35010  cdlemd3  35014  cdlemd4  35015  cdlemd5  35016  cdlemd6  35017  cdlemd7  35018  cdleme00a  35023  cdleme0cp  35028  cdleme0cq  35029  cdleme0e  35031  cdleme02N  35036  cdleme0ex2N  35038  cdleme0moN  35039  cdleme1  35041  cdleme2  35042  cdleme3e  35046  cdleme3g  35048  cdleme3h  35049  cdleme4  35052  cdleme5  35054  cdleme7aa  35056  cdleme7c  35059  cdleme7d  35060  cdleme7e  35061  cdleme8  35064  cdleme9  35067  cdleme10  35068  cdleme16aN  35073  cdleme11a  35074  cdleme11c  35075  cdleme11dN  35076  cdleme11e  35077  cdleme11g  35079  cdleme11h  35080  cdleme11j  35081  cdleme11k  35082  cdleme12  35085  cdleme15a  35088  cdleme15b  35089  cdleme16b  35093  cdleme17c  35102  cdleme0nex  35104  cdleme18d  35109  cdlemednpq  35113  cdleme20zN  35115  cdleme20y  35116  cdleme19a  35117  cdleme19d  35120  cdleme20aN  35123  cdleme20c  35125  cdleme20i  35131  cdleme20j  35132  cdleme21a  35139  cdleme21b  35140  cdleme21c  35141  cdleme21ct  35143  cdleme22cN  35156  cdleme22d  35157  cdleme22e  35158  cdleme22eALTN  35159  cdleme22f  35160  cdleme22f2  35161  cdleme22g  35162  cdleme23c  35165  cdleme41sn3a  35247  cdleme32le  35261  cdleme35b  35264  cdleme35c  35265  cdleme35d  35266  cdleme35e  35267  cdleme36a  35274  cdleme37m  35276  cdleme39a  35279  cdleme42a  35285  cdleme17d2  35309  cdlemeg46frv  35339  cdlemeg46rgv  35342  cdlemf1  35375  cdlemg2fv2  35414  cdlemg2l  35417  cdlemg2m  35418  cdlemg4d  35427  cdlemg4e  35428  cdlemg4f  35429  cdlemg4  35431  cdlemg6c  35434  cdlemg9a  35446  cdlemg10bALTN  35450  cdlemg12a  35457  cdlemg13  35466  cdlemg14f  35467  cdlemg14g  35468  cdlemg17i  35483  cdlemg17pq  35486  cdlemg19  35498  cdlemg21  35500  cdlemg27b  35510  cdlemg33c  35522  cdlemg33d  35523  trlcoabs2N  35536  cdlemg43  35544  cdlemg44b  35546  cdlemg44  35547  cdlemh1  35629  cdlemh2  35630  cdlemi1  35632  tendo0mul  35640  tendo0mulr  35641  cdlemk4  35648  cdlemk9  35653  cdlemk9bN  35654  cdlemk14  35668  cdlemkfid1N  35735  cdlemkid1  35736  cdlemk35s-id  35752  cdlemk39s-id  35754  cdlemk55a  35773  cdlemk55u  35780  cdlemk39u  35782  cdlemk19u  35784  cdlemk56  35785  cdleml8  35797  dia2dimlem1  35879  dia2dimlem2  35880  dia2dimlem3  35881  cdlemn10  36021  dihjust  36032  dihord1  36033  dihlsscpre  36049  dihvalcqpre  36050  dihglbcpreN  36115  dihmeetlem5  36123  dihmeetlem7N  36125  dihjatc1  36126
  Copyright terms: Public domain W3C validator