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

Theorem syl121anc 1355
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 504 . 2 (𝜑 → (𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl121anc.5 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ 𝜏) → 𝜂)
71, 4, 5, 6syl3anc 1351 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  w3a 1068
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 199  df-an 388  df-3an 1070
This theorem is referenced by:  syl122anc  1359  fsnunf2  6777  tfisi  7391  fnsuppeq0  7663  axdc4lem  9677  div32d  11242  div13d  11243  expdivd  13342  swrdsbslen  13844  sumeven  15601  sumodd  15602  pcqmul  16049  pcid  16068  pcneg  16069  pc2dvds  16074  pcz  16076  pcaddlem  16083  pcadd  16084  pcmpt2  16088  pcbc  16095  qexpz  16096  expnprm  16097  sylow1lem1  18487  lspsneleq  19612  lspsneq  19619  lspfixed  19625  frlmsslss2  20624  chmatval  21144  chpmat1dlem  21150  chpdmatlem2  21154  ucncn  22600  ucnextcn  22619  ssblex  22744  prdsxmslem2  22845  ncvs1  23467  voliunlem1  23857  deg1mul3le  24416  deg1pw  24420  fta1blem  24468  bcmono  25558  dchrisum0flblem1  25789  dchrisum0flblem2  25790  pntibndlem1  25870  pntlemr  25883  finsumvtxdg2sstep  27037  umgr3cyclex  27715  nv1  28232  resf1o  30221  omndmul3  30432  rngurd  30536  measun  31115  measvuni  31118  measunl  31120  nosupbnd1  32735  slerec  32798  btwnconn1lem14  33082  segcon2  33087  seglelin  33098  neibastop3  33231  upixp  34446  fdc  34462  eqlkr3  35682  lkrshp  35686  lfl1dim  35702  lfl1dim2N  35703  eqlkr4  35746  2llnneN  35990  3dim2  36049  4atlem3  36177  4atlem11  36190  4atlem12  36193  pexmidlem4N  36554  lhp2at0nle  36616  lhple  36623  ltrnideq  36756  cdlemd9  36787  cdleme0ex2N  36805  cdleme0moN  36806  cdleme11a  36841  cdleme30a  36959  cdlemefs32sn1aw  36995  cdleme43fsv1snlem  37001  cdlemefs31fv1  37005  cdlemefs45eN  37012  cdleme41sn3a  37014  cdleme35h  37037  cdleme36a  37041  cdleme40m  37048  cdleme40n  37049  cdleme41sn3aw  37055  cdleme42h  37063  cdleme42k  37065  cdleme42mN  37068  cdleme43cN  37072  cdleme17d3  37077  cdleme48fvg  37081  cdlemeg47rv2  37091  cdlemeg46c  37094  cdlemeg46sfg  37101  cdlemeg46rjgN  37103  cdlemeg46rgv  37109  cdlemeg46req  37110  cdlemeg46gfv  37111  cdlemeg46gfre  37113  cdlemeg49lebilem  37120  cdleme50trn2  37132  cdlemg2kq  37183  cdlemb3  37187  cdlemg4f  37196  cdlemg9a  37213  cdlemg9b  37214  cdlemg9  37215  cdlemg11aq  37219  cdlemg12a  37224  cdlemg12b  37225  cdlemg12c  37226  cdlemg12d  37227  cdlemg12f  37229  cdlemg12g  37230  cdlemg12  37231  cdlemg13a  37232  cdlemg16  37238  cdlemg17e  37246  cdlemg17f  37247  cdlemg17g  37248  cdlemg17ir  37251  cdlemg17  37258  cdlemg18b  37260  cdlemg18c  37261  cdlemg33e  37291  trlcoabs2N  37303  trlcocnvat  37305  trlcolem  37307  trlco  37308  cdlemg44  37314  cdlemg47  37317  ltrncom  37319  tendococl  37353  tendoplcl  37362  tendoplcom  37363  tendoplass  37364  tendodi1  37365  tendodi2  37366  tendo0pl  37372  tendoipl  37378  cdlemh1  37396  cdlemi2  37400  tendo0mul  37407  tendo0mulr  37408  cdlemk2  37413  cdlemk3  37414  cdlemk4  37415  cdlemk6  37418  cdlemk8  37419  cdlemk12  37431  cdlemkole  37434  cdlemk14  37435  cdlemk15  37436  cdlemk5u  37442  cdlemk6u  37443  cdlemk12u  37453  cdlemkfid1N  37502  cdlemk19x  37524  cdlemk48  37531  cdlemk53a  37536  cdlemk56  37552  cdleml2N  37558  cdleml3N  37559  cdleml6  37562  cdleml7  37563  dva1dim  37566  dia2dimlem4  37648  dvhlveclem  37689  doca2N  37707  djajN  37718  cdlemn2a  37777  cdlemn3  37778  dihordlem6  37794  dihord5apre  37843  dihglbcpreN  37881  dihmeetcN  37883  dihmeetbN  37884  dihmeetlem10N  37897  dihmeetlem12N  37899  dihmeetlem15N  37902  dihmeetALTN  37908  dih1dimatlem0  37909  dihjatcclem3  38001  dihjatcclem4  38002  mapdpglem22  38274  hdmap14lem1a  38447  eldioph2b  38755  jm2.19lem4  38985  jm2.19  38986  jm2.26a  38993  jm2.26  38995  hbtlem2  39120  fnchoice  40705  stoweidlem42  41759  stoweidlem59  41776  fourierdlem42  41866
  Copyright terms: Public domain W3C validator