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

Theorem syl121anc 1372
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl121anc.5 ((𝜓 ∧ (𝜒𝜃) ∧ 𝜏) → 𝜂)
Assertion
Ref Expression
syl121anc (𝜑𝜂)

Proof of Theorem syl121anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
42, 3jca 515 . 2 (𝜑 → (𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl121anc.5 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ 𝜏) → 𝜂)
71, 4, 5, 6syl3anc 1368 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  syl122anc  1376  fsnunf2  6939  tfisi  7567  fnsuppeq0  7854  axdc4lem  9875  div32d  11437  div13d  11438  expdivd  13529  swrdsbslen  14026  sumeven  15736  sumodd  15737  pcqmul  16188  pcid  16207  pcneg  16208  pc2dvds  16213  pcz  16215  pcaddlem  16222  pcadd  16223  pcmpt2  16227  pcbc  16234  qexpz  16235  expnprm  16236  sylow1lem1  18723  lspsneleq  19887  lspsneq  19894  lspfixed  19900  frlmsslss2  20471  chmatval  21440  chpmat1dlem  21446  chpdmatlem2  21450  ucncn  22897  ucnextcn  22916  ssblex  23041  prdsxmslem2  23142  ncvs1  23768  voliunlem1  24160  deg1mul3le  24723  deg1pw  24727  fta1blem  24775  bcmono  25867  dchrisum0flblem1  26098  dchrisum0flblem2  26099  pntibndlem1  26179  pntlemr  26192  finsumvtxdg2sstep  27345  umgr3cyclex  27974  nv1  28464  resf1o  30480  omndmul3  30749  symgcntz  30764  cycpmco2lem6  30808  tocyccntz  30821  rngurd  30892  measun  31530  measvuni  31533  measunl  31535  nosupbnd1  33274  slerec  33337  btwnconn1lem14  33621  segcon2  33626  seglelin  33637  neibastop3  33770  upixp  35115  fdc  35131  eqlkr3  36345  lkrshp  36349  lfl1dim  36365  lfl1dim2N  36366  eqlkr4  36409  2llnneN  36653  3dim2  36712  4atlem3  36840  4atlem11  36853  4atlem12  36856  pexmidlem4N  37217  lhp2at0nle  37279  lhple  37286  ltrnideq  37419  cdlemd9  37450  cdleme0ex2N  37468  cdleme0moN  37469  cdleme11a  37504  cdleme30a  37622  cdlemefs32sn1aw  37658  cdleme43fsv1snlem  37664  cdlemefs31fv1  37668  cdlemefs45eN  37675  cdleme41sn3a  37677  cdleme35h  37700  cdleme36a  37704  cdleme40m  37711  cdleme40n  37712  cdleme41sn3aw  37718  cdleme42h  37726  cdleme42k  37728  cdleme42mN  37731  cdleme43cN  37735  cdleme17d3  37740  cdleme48fvg  37744  cdlemeg47rv2  37754  cdlemeg46c  37757  cdlemeg46sfg  37764  cdlemeg46rjgN  37766  cdlemeg46rgv  37772  cdlemeg46req  37773  cdlemeg46gfv  37774  cdlemeg46gfre  37776  cdlemeg49lebilem  37783  cdleme50trn2  37795  cdlemg2kq  37846  cdlemb3  37850  cdlemg4f  37859  cdlemg9a  37876  cdlemg9b  37877  cdlemg9  37878  cdlemg11aq  37882  cdlemg12a  37887  cdlemg12b  37888  cdlemg12c  37889  cdlemg12d  37890  cdlemg12f  37892  cdlemg12g  37893  cdlemg12  37894  cdlemg13a  37895  cdlemg16  37901  cdlemg17e  37909  cdlemg17f  37910  cdlemg17g  37911  cdlemg17ir  37914  cdlemg17  37921  cdlemg18b  37923  cdlemg18c  37924  cdlemg33e  37954  trlcoabs2N  37966  trlcocnvat  37968  trlcolem  37970  trlco  37971  cdlemg44  37977  cdlemg47  37980  ltrncom  37982  tendococl  38016  tendoplcl  38025  tendoplcom  38026  tendoplass  38027  tendodi1  38028  tendodi2  38029  tendo0pl  38035  tendoipl  38041  cdlemh1  38059  cdlemi2  38063  tendo0mul  38070  tendo0mulr  38071  cdlemk2  38076  cdlemk3  38077  cdlemk4  38078  cdlemk6  38081  cdlemk8  38082  cdlemk12  38094  cdlemkole  38097  cdlemk14  38098  cdlemk15  38099  cdlemk5u  38105  cdlemk6u  38106  cdlemk12u  38116  cdlemkfid1N  38165  cdlemk19x  38187  cdlemk48  38194  cdlemk53a  38199  cdlemk56  38215  cdleml2N  38221  cdleml3N  38222  cdleml6  38225  cdleml7  38226  dva1dim  38229  dia2dimlem4  38311  dvhlveclem  38352  doca2N  38370  djajN  38381  cdlemn2a  38440  cdlemn3  38441  dihordlem6  38457  dihord5apre  38506  dihglbcpreN  38544  dihmeetcN  38546  dihmeetbN  38547  dihmeetlem10N  38560  dihmeetlem12N  38562  dihmeetlem15N  38565  dihmeetALTN  38571  dih1dimatlem0  38572  dihjatcclem3  38664  dihjatcclem4  38665  mapdpglem22  38937  hdmap14lem1a  39110  eldioph2b  39624  jm2.19lem4  39853  jm2.19  39854  jm2.26a  39861  jm2.26  39863  hbtlem2  39988  fnchoice  41582  stoweidlem42  42614  stoweidlem59  42631  fourierdlem42  42721
  Copyright terms: Public domain W3C validator