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

Theorem syl121anc 1273
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 535 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1268 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  syl122anc  1277  disjxiun  4399  fsnunf2  6103  tfisi  6685  fnsuppeq0  6943  axdc4lem  8885  div32d  10406  div13d  10407  expdivd  12430  swrdsbslen  12804  pcqmul  14803  pcid  14822  pcneg  14823  pc2dvds  14828  pcz  14830  pcaddlem  14833  pcadd  14834  pcmpt2  14838  pcbc  14845  qexpz  14846  expnprm  14847  sylow1lem1  17250  lspsneleq  18338  lspsneq  18345  lspfixed  18351  frlmsslss2  19333  chmatval  19853  chpmat1dlem  19859  chpdmatlem2  19863  ucncn  21300  ucnextcn  21319  ssblex  21443  prdsxmslem2  21544  voliunlem1  22503  deg1mul3le  23065  deg1pw  23069  fta1blem  23119  bcmono  24205  dchrisum0flblem1  24346  dchrisum0flblem2  24347  pntibndlem1  24427  pntlemr  24440  0wlkon  25277  0pthon  25309  clwlkfclwwlk  25572  nv1  26305  resf1o  28315  omndmul3  28476  rngurd  28551  measun  29033  measvuni  29036  measunl  29038  btwnconn1lem14  30867  segcon2  30872  seglelin  30883  neibastop3  31018  upixp  32056  fdc  32074  eqlkr3  32667  lkrshp  32671  lfl1dim  32687  lfl1dim2N  32688  eqlkr4  32731  2llnneN  32974  3dim2  33033  4atlem3  33161  4atlem11  33174  4atlem12  33177  pexmidlem4N  33538  lhp2at0nle  33600  lhple  33607  ltrnideq  33741  cdlemd9  33772  cdleme0ex2N  33790  cdleme0moN  33791  cdleme11a  33826  cdleme30a  33945  cdlemefs32sn1aw  33981  cdleme43fsv1snlem  33987  cdlemefs31fv1  33991  cdlemefs45eN  33998  cdleme41sn3a  34000  cdleme35h  34023  cdleme36a  34027  cdleme40m  34034  cdleme40n  34035  cdleme41sn3aw  34041  cdleme42h  34049  cdleme42k  34051  cdleme42mN  34054  cdleme43cN  34058  cdleme17d3  34063  cdleme48fvg  34067  cdlemeg47rv2  34077  cdlemeg46c  34080  cdlemeg46sfg  34087  cdlemeg46rjgN  34089  cdlemeg46rgv  34095  cdlemeg46req  34096  cdlemeg46gfv  34097  cdlemeg46gfre  34099  cdlemeg49lebilem  34106  cdleme50trn2  34118  cdlemg2kq  34169  cdlemb3  34173  cdlemg4f  34182  cdlemg9a  34199  cdlemg9b  34200  cdlemg9  34201  cdlemg11aq  34205  cdlemg12a  34210  cdlemg12b  34211  cdlemg12c  34212  cdlemg12d  34213  cdlemg12f  34215  cdlemg12g  34216  cdlemg12  34217  cdlemg13a  34218  cdlemg16  34224  cdlemg17e  34232  cdlemg17f  34233  cdlemg17g  34234  cdlemg17ir  34237  cdlemg17  34244  cdlemg18b  34246  cdlemg18c  34247  cdlemg33e  34277  trlcoabs2N  34289  trlcocnvat  34291  trlcolem  34293  trlco  34294  cdlemg44  34300  cdlemg47  34303  ltrncom  34305  tendococl  34339  tendoplcl  34348  tendoplcom  34349  tendoplass  34350  tendodi1  34351  tendodi2  34352  tendo0pl  34358  tendoipl  34364  cdlemh1  34382  cdlemi2  34386  tendo0mul  34393  tendo0mulr  34394  cdlemk2  34399  cdlemk3  34400  cdlemk4  34401  cdlemk6  34404  cdlemk8  34405  cdlemk12  34417  cdlemkole  34420  cdlemk14  34421  cdlemk15  34422  cdlemk5u  34428  cdlemk6u  34429  cdlemk12u  34439  cdlemkfid1N  34488  cdlemk19x  34510  cdlemk48  34517  cdlemk53a  34522  cdlemk56  34538  cdleml2N  34544  cdleml3N  34545  cdleml6  34548  cdleml7  34549  dva1dim  34552  dia2dimlem4  34635  dvhlveclem  34676  doca2N  34694  djajN  34705  cdlemn2a  34764  cdlemn3  34765  dihordlem6  34781  dihord5apre  34830  dihglbcpreN  34868  dihmeetcN  34870  dihmeetbN  34871  dihmeetlem10N  34884  dihmeetlem12N  34886  dihmeetlem15N  34889  dihmeetALTN  34895  dih1dimatlem0  34896  dihjatcclem3  34988  dihjatcclem4  34989  mapdpglem22  35261  hdmap14lem1a  35437  eldioph2b  35605  jm2.19lem4  35847  jm2.19  35848  jm2.26a  35855  jm2.26  35857  hbtlem2  35983  fnchoice  37350  stoweidlem42  37903  stoweidlem59  37920  fourierdlem42  38012  fourierdlem42OLD  38013
  Copyright terms: Public domain W3C validator