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

Theorem syl121anc 1371
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 553 . 2 (𝜑 → (𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl121anc.5 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ 𝜏) → 𝜂)
71, 4, 5, 6syl3anc 1366 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 1056
This theorem is referenced by:  syl122anc  1375  disjxiunOLD  4682  fsnunf2  6493  tfisi  7100  fnsuppeq0  7368  axdc4lem  9315  div32d  10862  div13d  10863  expdivd  13062  swrdsbslen  13494  sumeven  15157  sumodd  15158  pcqmul  15605  pcid  15624  pcneg  15625  pc2dvds  15630  pcz  15632  pcaddlem  15639  pcadd  15640  pcmpt2  15644  pcbc  15651  qexpz  15652  expnprm  15653  sylow1lem1  18059  lspsneleq  19163  lspsneq  19170  lspfixed  19176  frlmsslss2  20162  chmatval  20682  chpmat1dlem  20688  chpdmatlem2  20692  ucncn  22136  ucnextcn  22155  ssblex  22280  prdsxmslem2  22381  ncvs1  23003  voliunlem1  23364  deg1mul3le  23921  deg1pw  23925  fta1blem  23973  bcmono  25047  dchrisum0flblem1  25242  dchrisum0flblem2  25243  pntibndlem1  25323  pntlemr  25336  finsumvtxdg2sstep  26501  clwlksfclwwlk  27049  umgr3cyclex  27161  nv1  27658  resf1o  29633  omndmul3  29841  rngurd  29916  measun  30402  measvuni  30405  measunl  30407  nosupbnd1  31985  slerec  32048  btwnconn1lem14  32332  segcon2  32337  seglelin  32348  neibastop3  32482  upixp  33654  fdc  33671  eqlkr3  34706  lkrshp  34710  lfl1dim  34726  lfl1dim2N  34727  eqlkr4  34770  2llnneN  35013  3dim2  35072  4atlem3  35200  4atlem11  35213  4atlem12  35216  pexmidlem4N  35577  lhp2at0nle  35639  lhple  35646  ltrnideq  35780  cdlemd9  35811  cdleme0ex2N  35829  cdleme0moN  35830  cdleme11a  35865  cdleme30a  35983  cdlemefs32sn1aw  36019  cdleme43fsv1snlem  36025  cdlemefs31fv1  36029  cdlemefs45eN  36036  cdleme41sn3a  36038  cdleme35h  36061  cdleme36a  36065  cdleme40m  36072  cdleme40n  36073  cdleme41sn3aw  36079  cdleme42h  36087  cdleme42k  36089  cdleme42mN  36092  cdleme43cN  36096  cdleme17d3  36101  cdleme48fvg  36105  cdlemeg47rv2  36115  cdlemeg46c  36118  cdlemeg46sfg  36125  cdlemeg46rjgN  36127  cdlemeg46rgv  36133  cdlemeg46req  36134  cdlemeg46gfv  36135  cdlemeg46gfre  36137  cdlemeg49lebilem  36144  cdleme50trn2  36156  cdlemg2kq  36207  cdlemb3  36211  cdlemg4f  36220  cdlemg9a  36237  cdlemg9b  36238  cdlemg9  36239  cdlemg11aq  36243  cdlemg12a  36248  cdlemg12b  36249  cdlemg12c  36250  cdlemg12d  36251  cdlemg12f  36253  cdlemg12g  36254  cdlemg12  36255  cdlemg13a  36256  cdlemg16  36262  cdlemg17e  36270  cdlemg17f  36271  cdlemg17g  36272  cdlemg17ir  36275  cdlemg17  36282  cdlemg18b  36284  cdlemg18c  36285  cdlemg33e  36315  trlcoabs2N  36327  trlcocnvat  36329  trlcolem  36331  trlco  36332  cdlemg44  36338  cdlemg47  36341  ltrncom  36343  tendococl  36377  tendoplcl  36386  tendoplcom  36387  tendoplass  36388  tendodi1  36389  tendodi2  36390  tendo0pl  36396  tendoipl  36402  cdlemh1  36420  cdlemi2  36424  tendo0mul  36431  tendo0mulr  36432  cdlemk2  36437  cdlemk3  36438  cdlemk4  36439  cdlemk6  36442  cdlemk8  36443  cdlemk12  36455  cdlemkole  36458  cdlemk14  36459  cdlemk15  36460  cdlemk5u  36466  cdlemk6u  36467  cdlemk12u  36477  cdlemkfid1N  36526  cdlemk19x  36548  cdlemk48  36555  cdlemk53a  36560  cdlemk56  36576  cdleml2N  36582  cdleml3N  36583  cdleml6  36586  cdleml7  36587  dva1dim  36590  dia2dimlem4  36673  dvhlveclem  36714  doca2N  36732  djajN  36743  cdlemn2a  36802  cdlemn3  36803  dihordlem6  36819  dihord5apre  36868  dihglbcpreN  36906  dihmeetcN  36908  dihmeetbN  36909  dihmeetlem10N  36922  dihmeetlem12N  36924  dihmeetlem15N  36927  dihmeetALTN  36933  dih1dimatlem0  36934  dihjatcclem3  37026  dihjatcclem4  37027  mapdpglem22  37299  hdmap14lem1a  37475  eldioph2b  37643  jm2.19lem4  37876  jm2.19  37877  jm2.26a  37884  jm2.26  37886  hbtlem2  38011  fnchoice  39502  stoweidlem42  40577  stoweidlem59  40594  fourierdlem42  40684
  Copyright terms: Public domain W3C validator