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

Theorem syl121anc 1367
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 512 . 2 (𝜑 → (𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl121anc.5 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ 𝜏) → 𝜂)
71, 4, 5, 6syl3anc 1363 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  syl122anc  1371  fsnunf2  6940  tfisi  7562  fnsuppeq0  7847  axdc4lem  9865  div32d  11427  div13d  11428  expdivd  13512  swrdsbslen  14014  sumeven  15726  sumodd  15727  pcqmul  16178  pcid  16197  pcneg  16198  pc2dvds  16203  pcz  16205  pcaddlem  16212  pcadd  16213  pcmpt2  16217  pcbc  16224  qexpz  16225  expnprm  16226  sylow1lem1  18652  lspsneleq  19816  lspsneq  19823  lspfixed  19829  frlmsslss2  20847  chmatval  21365  chpmat1dlem  21371  chpdmatlem2  21375  ucncn  22821  ucnextcn  22840  ssblex  22965  prdsxmslem2  23066  ncvs1  23688  voliunlem1  24078  deg1mul3le  24637  deg1pw  24641  fta1blem  24689  bcmono  25780  dchrisum0flblem1  26011  dchrisum0flblem2  26012  pntibndlem1  26092  pntlemr  26105  finsumvtxdg2sstep  27258  umgr3cyclex  27889  nv1  28379  resf1o  30392  omndmul3  30641  symgcntz  30656  cycpmco2lem6  30700  tocyccntz  30713  rngurd  30784  measun  31369  measvuni  31372  measunl  31374  nosupbnd1  33111  slerec  33174  btwnconn1lem14  33458  segcon2  33463  seglelin  33474  neibastop3  33607  upixp  34885  fdc  34901  eqlkr3  36117  lkrshp  36121  lfl1dim  36137  lfl1dim2N  36138  eqlkr4  36181  2llnneN  36425  3dim2  36484  4atlem3  36612  4atlem11  36625  4atlem12  36628  pexmidlem4N  36989  lhp2at0nle  37051  lhple  37058  ltrnideq  37191  cdlemd9  37222  cdleme0ex2N  37240  cdleme0moN  37241  cdleme11a  37276  cdleme30a  37394  cdlemefs32sn1aw  37430  cdleme43fsv1snlem  37436  cdlemefs31fv1  37440  cdlemefs45eN  37447  cdleme41sn3a  37449  cdleme35h  37472  cdleme36a  37476  cdleme40m  37483  cdleme40n  37484  cdleme41sn3aw  37490  cdleme42h  37498  cdleme42k  37500  cdleme42mN  37503  cdleme43cN  37507  cdleme17d3  37512  cdleme48fvg  37516  cdlemeg47rv2  37526  cdlemeg46c  37529  cdlemeg46sfg  37536  cdlemeg46rjgN  37538  cdlemeg46rgv  37544  cdlemeg46req  37545  cdlemeg46gfv  37546  cdlemeg46gfre  37548  cdlemeg49lebilem  37555  cdleme50trn2  37567  cdlemg2kq  37618  cdlemb3  37622  cdlemg4f  37631  cdlemg9a  37648  cdlemg9b  37649  cdlemg9  37650  cdlemg11aq  37654  cdlemg12a  37659  cdlemg12b  37660  cdlemg12c  37661  cdlemg12d  37662  cdlemg12f  37664  cdlemg12g  37665  cdlemg12  37666  cdlemg13a  37667  cdlemg16  37673  cdlemg17e  37681  cdlemg17f  37682  cdlemg17g  37683  cdlemg17ir  37686  cdlemg17  37693  cdlemg18b  37695  cdlemg18c  37696  cdlemg33e  37726  trlcoabs2N  37738  trlcocnvat  37740  trlcolem  37742  trlco  37743  cdlemg44  37749  cdlemg47  37752  ltrncom  37754  tendococl  37788  tendoplcl  37797  tendoplcom  37798  tendoplass  37799  tendodi1  37800  tendodi2  37801  tendo0pl  37807  tendoipl  37813  cdlemh1  37831  cdlemi2  37835  tendo0mul  37842  tendo0mulr  37843  cdlemk2  37848  cdlemk3  37849  cdlemk4  37850  cdlemk6  37853  cdlemk8  37854  cdlemk12  37866  cdlemkole  37869  cdlemk14  37870  cdlemk15  37871  cdlemk5u  37877  cdlemk6u  37878  cdlemk12u  37888  cdlemkfid1N  37937  cdlemk19x  37959  cdlemk48  37966  cdlemk53a  37971  cdlemk56  37987  cdleml2N  37993  cdleml3N  37994  cdleml6  37997  cdleml7  37998  dva1dim  38001  dia2dimlem4  38083  dvhlveclem  38124  doca2N  38142  djajN  38153  cdlemn2a  38212  cdlemn3  38213  dihordlem6  38229  dihord5apre  38278  dihglbcpreN  38316  dihmeetcN  38318  dihmeetbN  38319  dihmeetlem10N  38332  dihmeetlem12N  38334  dihmeetlem15N  38337  dihmeetALTN  38343  dih1dimatlem0  38344  dihjatcclem3  38436  dihjatcclem4  38437  mapdpglem22  38709  hdmap14lem1a  38882  eldioph2b  39238  jm2.19lem4  39467  jm2.19  39468  jm2.26a  39475  jm2.26  39477  hbtlem2  39602  fnchoice  41163  stoweidlem42  42204  stoweidlem59  42221  fourierdlem42  42311
  Copyright terms: Public domain W3C validator