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

Theorem syl121anc 1216
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 529 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1211 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  syl122anc  1220  disjxiun  4277  fsnunf2  5904  tfisi  6458  fnsuppeq0  6706  axdc4lem  8612  div32d  10117  div13d  10118  expdivd  12005  pcqmul  13902  pcid  13921  pcneg  13922  pc2dvds  13927  pcz  13929  pcaddlem  13932  pcadd  13933  pcmpt2  13937  pcbc  13944  qexpz  13945  expnprm  13946  sylow1lem1  16076  lspsneleq  17117  lspsneq  17124  lspfixed  17130  frlmsslss2  18040  ucncn  19701  ucnextcn  19720  ssblex  19844  prdsxmslem2  19945  voliunlem1  20872  deg1mul3le  21472  deg1pw  21476  fta1blem  21524  bcmono  22500  dchrisum0flblem1  22641  dchrisum0flblem2  22642  pntibndlem1  22722  pntlemr  22735  0wlkon  23268  0pthon  23300  nv1  23886  omndmul3  25999  measun  26478  measvuni  26481  measunl  26483  btwnconn1lem14  27977  segcon2  27982  seglelin  27993  neibastop3  28424  upixp  28464  fdc  28482  eldioph2b  28943  jm2.19lem4  29183  jm2.19  29184  jm2.26a  29191  jm2.26  29193  hbtlem2  29322  fnchoice  29593  stoweidlem42  29680  stoweidlem59  29697  clwlkfclwwlk  30360  eqlkr3  32316  lkrshp  32320  lfl1dim  32336  lfl1dim2N  32337  eqlkr4  32380  2llnneN  32623  3dim2  32682  4atlem3  32810  4atlem11  32823  4atlem12  32826  pexmidlem4N  33187  lhp2at0nle  33249  lhple  33256  ltrnideq  33389  cdlemd9  33420  cdleme0ex2N  33438  cdleme0moN  33439  cdleme11a  33474  cdleme30a  33592  cdlemefs32sn1aw  33628  cdleme43fsv1snlem  33634  cdlemefs31fv1  33638  cdlemefs45eN  33645  cdleme41sn3a  33647  cdleme35h  33670  cdleme36a  33674  cdleme40m  33681  cdleme40n  33682  cdleme41sn3aw  33688  cdleme42h  33696  cdleme42k  33698  cdleme42mN  33701  cdleme43cN  33705  cdleme17d3  33710  cdleme48fvg  33714  cdlemeg47rv2  33724  cdlemeg46c  33727  cdlemeg46sfg  33734  cdlemeg46rjgN  33736  cdlemeg46rgv  33742  cdlemeg46req  33743  cdlemeg46gfv  33744  cdlemeg46gfre  33746  cdlemeg49lebilem  33753  cdleme50trn2  33765  cdlemg2kq  33816  cdlemb3  33820  cdlemg4f  33829  cdlemg9a  33846  cdlemg9b  33847  cdlemg9  33848  cdlemg11aq  33852  cdlemg12a  33857  cdlemg12b  33858  cdlemg12c  33859  cdlemg12d  33860  cdlemg12f  33862  cdlemg12g  33863  cdlemg12  33864  cdlemg13a  33865  cdlemg16  33871  cdlemg17e  33879  cdlemg17f  33880  cdlemg17g  33881  cdlemg17ir  33884  cdlemg17  33891  cdlemg18b  33893  cdlemg18c  33894  cdlemg33e  33924  trlcoabs2N  33936  trlcocnvat  33938  trlcolem  33940  trlco  33941  cdlemg44  33947  cdlemg47  33950  ltrncom  33952  tendococl  33986  tendoplcl  33995  tendoplcom  33996  tendoplass  33997  tendodi1  33998  tendodi2  33999  tendo0pl  34005  tendoipl  34011  cdlemh1  34029  cdlemi2  34033  tendo0mul  34040  tendo0mulr  34041  cdlemk2  34046  cdlemk3  34047  cdlemk4  34048  cdlemk6  34051  cdlemk8  34052  cdlemk12  34064  cdlemkole  34067  cdlemk14  34068  cdlemk15  34069  cdlemk5u  34075  cdlemk6u  34076  cdlemk12u  34086  cdlemkfid1N  34135  cdlemk19x  34157  cdlemk48  34164  cdlemk53a  34169  cdlemk56  34185  cdleml2N  34191  cdleml3N  34192  cdleml6  34195  cdleml7  34196  dva1dim  34199  dia2dimlem4  34282  dvhlveclem  34323  doca2N  34341  djajN  34352  cdlemn2a  34411  cdlemn3  34412  dihordlem6  34428  dihord5apre  34477  dihglbcpreN  34515  dihmeetcN  34517  dihmeetbN  34518  dihmeetlem10N  34531  dihmeetlem12N  34533  dihmeetlem15N  34536  dihmeetALTN  34542  dih1dimatlem0  34543  dihjatcclem3  34635  dihjatcclem4  34636  mapdpglem22  34908  hdmap14lem1a  35084
  Copyright terms: Public domain W3C validator