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

Theorem syl121anc 1189
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 519 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1184 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  syl122anc  1193  disjxiun  4201  tfisi  4830  fsnunf2  5924  axdc4lem  8327  div32d  9805  div13d  9806  expdivd  11529  pcqmul  13219  pcid  13238  pcneg  13239  pc2dvds  13244  pcz  13246  pcaddlem  13249  pcadd  13250  pcmpt2  13254  pcbc  13261  qexpz  13262  expnprm  13263  spwpr4c  14656  sylow1lem1  15224  lspsneleq  16179  lspsneq  16186  lspfixed  16192  ucncn  18307  ucnextcn  18326  ssblex  18450  prdsxmslem2  18551  voliunlem1  19436  deg1mul3le  20031  deg1pw  20035  fta1blem  20083  bcmono  21053  dchrisum0flblem1  21194  dchrisum0flblem2  21195  pntibndlem1  21275  pntlemr  21288  0wlkon  21539  0pthon  21571  nv1  22157  measun  24557  measvuni  24560  measunl  24562  btwnconn1lem14  26026  segcon2  26031  seglelin  26042  neibastop3  26372  upixp  26412  fdc  26430  eldioph2b  26802  jm2.19lem4  27044  jm2.19  27045  jm2.26a  27052  jm2.26  27054  hbtlem2  27286  fnchoice  27657  stoweidlem42  27748  stoweidlem59  27765  eqlkr3  29826  lkrshp  29830  lfl1dim  29846  lfl1dim2N  29847  eqlkr4  29890  2llnneN  30133  3dim2  30192  4atlem3  30320  4atlem11  30333  4atlem12  30336  pexmidlem4N  30697  lhp2at0nle  30759  lhple  30766  ltrnideq  30899  cdlemd9  30930  cdleme0ex2N  30948  cdleme0moN  30949  cdleme11a  30984  cdleme30a  31102  cdlemefs32sn1aw  31138  cdleme43fsv1snlem  31144  cdlemefs31fv1  31148  cdlemefs45eN  31155  cdleme41sn3a  31157  cdleme35h  31180  cdleme36a  31184  cdleme40m  31191  cdleme40n  31192  cdleme41sn3aw  31198  cdleme42h  31206  cdleme42k  31208  cdleme42mN  31211  cdleme43cN  31215  cdleme17d3  31220  cdleme48fvg  31224  cdlemeg47rv2  31234  cdlemeg46c  31237  cdlemeg46sfg  31244  cdlemeg46rjgN  31246  cdlemeg46rgv  31252  cdlemeg46req  31253  cdlemeg46gfv  31254  cdlemeg46gfre  31256  cdlemeg49lebilem  31263  cdleme50trn2  31275  cdlemg2kq  31326  cdlemb3  31330  cdlemg4f  31339  cdlemg9a  31356  cdlemg9b  31357  cdlemg9  31358  cdlemg11aq  31362  cdlemg12a  31367  cdlemg12b  31368  cdlemg12c  31369  cdlemg12d  31370  cdlemg12f  31372  cdlemg12g  31373  cdlemg12  31374  cdlemg13a  31375  cdlemg16  31381  cdlemg17e  31389  cdlemg17f  31390  cdlemg17g  31391  cdlemg17ir  31394  cdlemg17  31401  cdlemg18b  31403  cdlemg18c  31404  cdlemg33e  31434  trlcoabs2N  31446  trlcocnvat  31448  trlcolem  31450  trlco  31451  cdlemg44  31457  cdlemg47  31460  ltrncom  31462  tendococl  31496  tendoplcl  31505  tendoplcom  31506  tendoplass  31507  tendodi1  31508  tendodi2  31509  tendo0pl  31515  tendoipl  31521  cdlemh1  31539  cdlemi2  31543  tendo0mul  31550  tendo0mulr  31551  cdlemk2  31556  cdlemk3  31557  cdlemk4  31558  cdlemk6  31561  cdlemk8  31562  cdlemk12  31574  cdlemkole  31577  cdlemk14  31578  cdlemk15  31579  cdlemk5u  31585  cdlemk6u  31586  cdlemk12u  31596  cdlemkfid1N  31645  cdlemk19x  31667  cdlemk48  31674  cdlemk53a  31679  cdlemk56  31695  cdleml2N  31701  cdleml3N  31702  cdleml6  31705  cdleml7  31706  dva1dim  31709  dia2dimlem4  31792  dvhlveclem  31833  doca2N  31851  djajN  31862  cdlemn2a  31921  cdlemn3  31922  dihordlem6  31938  dihord5apre  31987  dihglbcpreN  32025  dihmeetcN  32027  dihmeetbN  32028  dihmeetlem10N  32041  dihmeetlem12N  32043  dihmeetlem15N  32046  dihmeetALTN  32052  dih1dimatlem0  32053  dihjatcclem3  32145  dihjatcclem4  32146  mapdpglem22  32418  hdmap14lem1a  32594
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator