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

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

Proof of Theorem syl121anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
42, 3jca 555 . 2 (𝜑 → (𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl121anc.5 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ 𝜏) → 𝜂)
71, 4, 5, 6syl3anc 1473 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  syl122anc  1482  fsnunf2  6608  tfisi  7215  fnsuppeq0  7484  axdc4lem  9461  div32d  11008  div13d  11009  expdivd  13208  swrdsbslen  13640  sumeven  15304  sumodd  15305  pcqmul  15752  pcid  15771  pcneg  15772  pc2dvds  15777  pcz  15779  pcaddlem  15786  pcadd  15787  pcmpt2  15791  pcbc  15798  qexpz  15799  expnprm  15800  sylow1lem1  18205  lspsneleq  19309  lspsneq  19316  lspfixed  19322  frlmsslss2  20308  chmatval  20828  chpmat1dlem  20834  chpdmatlem2  20838  ucncn  22282  ucnextcn  22301  ssblex  22426  prdsxmslem2  22527  ncvs1  23149  voliunlem1  23510  deg1mul3le  24067  deg1pw  24071  fta1blem  24119  bcmono  25193  dchrisum0flblem1  25388  dchrisum0flblem2  25389  pntibndlem1  25469  pntlemr  25482  finsumvtxdg2sstep  26647  clwlksfclwwlkOLD  27208  umgr3cyclex  27327  nv1  27831  resf1o  29806  omndmul3  30014  rngurd  30089  measun  30575  measvuni  30578  measunl  30580  nosupbnd1  32158  slerec  32221  btwnconn1lem14  32505  segcon2  32510  seglelin  32521  neibastop3  32655  upixp  33829  fdc  33846  eqlkr3  34883  lkrshp  34887  lfl1dim  34903  lfl1dim2N  34904  eqlkr4  34947  2llnneN  35190  3dim2  35249  4atlem3  35377  4atlem11  35390  4atlem12  35393  pexmidlem4N  35754  lhp2at0nle  35816  lhple  35823  ltrnideq  35957  cdlemd9  35988  cdleme0ex2N  36006  cdleme0moN  36007  cdleme11a  36042  cdleme30a  36160  cdlemefs32sn1aw  36196  cdleme43fsv1snlem  36202  cdlemefs31fv1  36206  cdlemefs45eN  36213  cdleme41sn3a  36215  cdleme35h  36238  cdleme36a  36242  cdleme40m  36249  cdleme40n  36250  cdleme41sn3aw  36256  cdleme42h  36264  cdleme42k  36266  cdleme42mN  36269  cdleme43cN  36273  cdleme17d3  36278  cdleme48fvg  36282  cdlemeg47rv2  36292  cdlemeg46c  36295  cdlemeg46sfg  36302  cdlemeg46rjgN  36304  cdlemeg46rgv  36310  cdlemeg46req  36311  cdlemeg46gfv  36312  cdlemeg46gfre  36314  cdlemeg49lebilem  36321  cdleme50trn2  36333  cdlemg2kq  36384  cdlemb3  36388  cdlemg4f  36397  cdlemg9a  36414  cdlemg9b  36415  cdlemg9  36416  cdlemg11aq  36420  cdlemg12a  36425  cdlemg12b  36426  cdlemg12c  36427  cdlemg12d  36428  cdlemg12f  36430  cdlemg12g  36431  cdlemg12  36432  cdlemg13a  36433  cdlemg16  36439  cdlemg17e  36447  cdlemg17f  36448  cdlemg17g  36449  cdlemg17ir  36452  cdlemg17  36459  cdlemg18b  36461  cdlemg18c  36462  cdlemg33e  36492  trlcoabs2N  36504  trlcocnvat  36506  trlcolem  36508  trlco  36509  cdlemg44  36515  cdlemg47  36518  ltrncom  36520  tendococl  36554  tendoplcl  36563  tendoplcom  36564  tendoplass  36565  tendodi1  36566  tendodi2  36567  tendo0pl  36573  tendoipl  36579  cdlemh1  36597  cdlemi2  36601  tendo0mul  36608  tendo0mulr  36609  cdlemk2  36614  cdlemk3  36615  cdlemk4  36616  cdlemk6  36619  cdlemk8  36620  cdlemk12  36632  cdlemkole  36635  cdlemk14  36636  cdlemk15  36637  cdlemk5u  36643  cdlemk6u  36644  cdlemk12u  36654  cdlemkfid1N  36703  cdlemk19x  36725  cdlemk48  36732  cdlemk53a  36737  cdlemk56  36753  cdleml2N  36759  cdleml3N  36760  cdleml6  36763  cdleml7  36764  dva1dim  36767  dia2dimlem4  36850  dvhlveclem  36891  doca2N  36909  djajN  36920  cdlemn2a  36979  cdlemn3  36980  dihordlem6  36996  dihord5apre  37045  dihglbcpreN  37083  dihmeetcN  37085  dihmeetbN  37086  dihmeetlem10N  37099  dihmeetlem12N  37101  dihmeetlem15N  37104  dihmeetALTN  37110  dih1dimatlem0  37111  dihjatcclem3  37203  dihjatcclem4  37204  mapdpglem22  37476  hdmap14lem1a  37652  eldioph2b  37820  jm2.19lem4  38053  jm2.19  38054  jm2.26a  38061  jm2.26  38063  hbtlem2  38188  fnchoice  39679  stoweidlem42  40754  stoweidlem59  40771  fourierdlem42  40861
  Copyright terms: Public domain W3C validator