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

Theorem syl121anc 1323
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 1318 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  syl122anc  1327  disjxiunOLD  4575  fsnunf2  6335  tfisi  6928  fnsuppeq0  7188  axdc4lem  9138  div32d  10676  div13d  10677  expdivd  12842  swrdsbslen  13249  pcqmul  15345  pcid  15364  pcneg  15365  pc2dvds  15370  pcz  15372  pcaddlem  15379  pcadd  15380  pcmpt2  15384  pcbc  15391  qexpz  15392  expnprm  15393  sylow1lem1  17785  lspsneleq  18885  lspsneq  18892  lspfixed  18898  frlmsslss2  19881  chmatval  20401  chpmat1dlem  20407  chpdmatlem2  20411  ucncn  21847  ucnextcn  21866  ssblex  21991  prdsxmslem2  22092  ncvs1  22710  voliunlem1  23070  deg1mul3le  23625  deg1pw  23629  fta1blem  23677  bcmono  24747  dchrisum0flblem1  24942  dchrisum0flblem2  24943  pntibndlem1  25023  pntlemr  25036  0wlkon  25871  0pthon  25903  clwlkfclwwlk  26165  nv1  26708  resf1o  28687  omndmul3  28838  rngurd  28913  measun  29395  measvuni  29398  measunl  29400  btwnconn1lem14  31171  segcon2  31176  seglelin  31187  neibastop3  31321  upixp  32488  fdc  32505  eqlkr3  33200  lkrshp  33204  lfl1dim  33220  lfl1dim2N  33221  eqlkr4  33264  2llnneN  33507  3dim2  33566  4atlem3  33694  4atlem11  33707  4atlem12  33710  pexmidlem4N  34071  lhp2at0nle  34133  lhple  34140  ltrnideq  34274  cdlemd9  34305  cdleme0ex2N  34323  cdleme0moN  34324  cdleme11a  34359  cdleme30a  34478  cdlemefs32sn1aw  34514  cdleme43fsv1snlem  34520  cdlemefs31fv1  34524  cdlemefs45eN  34531  cdleme41sn3a  34533  cdleme35h  34556  cdleme36a  34560  cdleme40m  34567  cdleme40n  34568  cdleme41sn3aw  34574  cdleme42h  34582  cdleme42k  34584  cdleme42mN  34587  cdleme43cN  34591  cdleme17d3  34596  cdleme48fvg  34600  cdlemeg47rv2  34610  cdlemeg46c  34613  cdlemeg46sfg  34620  cdlemeg46rjgN  34622  cdlemeg46rgv  34628  cdlemeg46req  34629  cdlemeg46gfv  34630  cdlemeg46gfre  34632  cdlemeg49lebilem  34639  cdleme50trn2  34651  cdlemg2kq  34702  cdlemb3  34706  cdlemg4f  34715  cdlemg9a  34732  cdlemg9b  34733  cdlemg9  34734  cdlemg11aq  34738  cdlemg12a  34743  cdlemg12b  34744  cdlemg12c  34745  cdlemg12d  34746  cdlemg12f  34748  cdlemg12g  34749  cdlemg12  34750  cdlemg13a  34751  cdlemg16  34757  cdlemg17e  34765  cdlemg17f  34766  cdlemg17g  34767  cdlemg17ir  34770  cdlemg17  34777  cdlemg18b  34779  cdlemg18c  34780  cdlemg33e  34810  trlcoabs2N  34822  trlcocnvat  34824  trlcolem  34826  trlco  34827  cdlemg44  34833  cdlemg47  34836  ltrncom  34838  tendococl  34872  tendoplcl  34881  tendoplcom  34882  tendoplass  34883  tendodi1  34884  tendodi2  34885  tendo0pl  34891  tendoipl  34897  cdlemh1  34915  cdlemi2  34919  tendo0mul  34926  tendo0mulr  34927  cdlemk2  34932  cdlemk3  34933  cdlemk4  34934  cdlemk6  34937  cdlemk8  34938  cdlemk12  34950  cdlemkole  34953  cdlemk14  34954  cdlemk15  34955  cdlemk5u  34961  cdlemk6u  34962  cdlemk12u  34972  cdlemkfid1N  35021  cdlemk19x  35043  cdlemk48  35050  cdlemk53a  35055  cdlemk56  35071  cdleml2N  35077  cdleml3N  35078  cdleml6  35081  cdleml7  35082  dva1dim  35085  dia2dimlem4  35168  dvhlveclem  35209  doca2N  35227  djajN  35238  cdlemn2a  35297  cdlemn3  35298  dihordlem6  35314  dihord5apre  35363  dihglbcpreN  35401  dihmeetcN  35403  dihmeetbN  35404  dihmeetlem10N  35417  dihmeetlem12N  35419  dihmeetlem15N  35422  dihmeetALTN  35428  dih1dimatlem0  35429  dihjatcclem3  35521  dihjatcclem4  35522  mapdpglem22  35794  hdmap14lem1a  35970  eldioph2b  36138  jm2.19lem4  36371  jm2.19  36372  jm2.26a  36379  jm2.26  36381  hbtlem2  36507  fnchoice  38005  stoweidlem42  38729  stoweidlem59  38746  fourierdlem42  38836  clwlksfclwwlk  41261  umgr3cyclex  41342
  Copyright terms: Public domain W3C validator