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

Theorem syl121anc 1233
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 )
syl121anc.5  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
Assertion
Ref Expression
syl121anc  |-  ( ph  ->  et )

Proof of Theorem syl121anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
42, 3jca 532 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1228 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ 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:  syl122anc  1237  disjxiun  4444  fsnunf2  6100  tfisi  6677  fnsuppeq0  6928  axdc4lem  8835  div32d  10343  div13d  10344  expdivd  12292  pcqmul  14236  pcid  14255  pcneg  14256  pc2dvds  14261  pcz  14263  pcaddlem  14266  pcadd  14267  pcmpt2  14271  pcbc  14278  qexpz  14279  expnprm  14280  sylow1lem1  16424  lspsneleq  17561  lspsneq  17568  lspfixed  17574  frlmsslss2  18600  chmatval  19125  chpmat1dlem  19131  chpdmatlem2  19135  ucncn  20551  ucnextcn  20570  ssblex  20694  prdsxmslem2  20795  voliunlem1  21723  deg1mul3le  22280  deg1pw  22284  fta1blem  22332  bcmono  23308  dchrisum0flblem1  23449  dchrisum0flblem2  23450  pntibndlem1  23530  pntlemr  23543  0wlkon  24253  0pthon  24285  clwlkfclwwlk  24548  nv1  25283  resf1o  27253  omndmul3  27393  measun  27850  measvuni  27853  measunl  27855  btwnconn1lem14  29355  segcon2  29360  seglelin  29371  neibastop3  29811  upixp  29851  fdc  29869  eldioph2b  30328  jm2.19lem4  30566  jm2.19  30567  jm2.26a  30574  jm2.26  30576  hbtlem2  30705  fnchoice  31010  stoweidlem42  31370  stoweidlem59  31387  eqlkr3  33916  lkrshp  33920  lfl1dim  33936  lfl1dim2N  33937  eqlkr4  33980  2llnneN  34223  3dim2  34282  4atlem3  34410  4atlem11  34423  4atlem12  34426  pexmidlem4N  34787  lhp2at0nle  34849  lhple  34856  ltrnideq  34989  cdlemd9  35020  cdleme0ex2N  35038  cdleme0moN  35039  cdleme11a  35074  cdleme30a  35192  cdlemefs32sn1aw  35228  cdleme43fsv1snlem  35234  cdlemefs31fv1  35238  cdlemefs45eN  35245  cdleme41sn3a  35247  cdleme35h  35270  cdleme36a  35274  cdleme40m  35281  cdleme40n  35282  cdleme41sn3aw  35288  cdleme42h  35296  cdleme42k  35298  cdleme42mN  35301  cdleme43cN  35305  cdleme17d3  35310  cdleme48fvg  35314  cdlemeg47rv2  35324  cdlemeg46c  35327  cdlemeg46sfg  35334  cdlemeg46rjgN  35336  cdlemeg46rgv  35342  cdlemeg46req  35343  cdlemeg46gfv  35344  cdlemeg46gfre  35346  cdlemeg49lebilem  35353  cdleme50trn2  35365  cdlemg2kq  35416  cdlemb3  35420  cdlemg4f  35429  cdlemg9a  35446  cdlemg9b  35447  cdlemg9  35448  cdlemg11aq  35452  cdlemg12a  35457  cdlemg12b  35458  cdlemg12c  35459  cdlemg12d  35460  cdlemg12f  35462  cdlemg12g  35463  cdlemg12  35464  cdlemg13a  35465  cdlemg16  35471  cdlemg17e  35479  cdlemg17f  35480  cdlemg17g  35481  cdlemg17ir  35484  cdlemg17  35491  cdlemg18b  35493  cdlemg18c  35494  cdlemg33e  35524  trlcoabs2N  35536  trlcocnvat  35538  trlcolem  35540  trlco  35541  cdlemg44  35547  cdlemg47  35550  ltrncom  35552  tendococl  35586  tendoplcl  35595  tendoplcom  35596  tendoplass  35597  tendodi1  35598  tendodi2  35599  tendo0pl  35605  tendoipl  35611  cdlemh1  35629  cdlemi2  35633  tendo0mul  35640  tendo0mulr  35641  cdlemk2  35646  cdlemk3  35647  cdlemk4  35648  cdlemk6  35651  cdlemk8  35652  cdlemk12  35664  cdlemkole  35667  cdlemk14  35668  cdlemk15  35669  cdlemk5u  35675  cdlemk6u  35676  cdlemk12u  35686  cdlemkfid1N  35735  cdlemk19x  35757  cdlemk48  35764  cdlemk53a  35769  cdlemk56  35785  cdleml2N  35791  cdleml3N  35792  cdleml6  35795  cdleml7  35796  dva1dim  35799  dia2dimlem4  35882  dvhlveclem  35923  doca2N  35941  djajN  35952  cdlemn2a  36011  cdlemn3  36012  dihordlem6  36028  dihord5apre  36077  dihglbcpreN  36115  dihmeetcN  36117  dihmeetbN  36118  dihmeetlem10N  36131  dihmeetlem12N  36133  dihmeetlem15N  36136  dihmeetALTN  36142  dih1dimatlem0  36143  dihjatcclem3  36235  dihjatcclem4  36236  mapdpglem22  36508  hdmap14lem1a  36684
  Copyright terms: Public domain W3C validator