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

Theorem syl121anc 1376
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 513 . 2 (𝜑 → (𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl121anc.5 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ 𝜏) → 𝜂)
71, 4, 5, 6syl3anc 1372 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  syl122anc  1380  fsnunf2  7137  tfisi  7800  fnsuppeq0  8128  ttrclss  9663  ttrclselem2  9669  axdc4lem  10398  div32d  11961  div13d  11962  expdivd  14072  swrdsbslen  14559  sumeven  16276  sumodd  16277  pcqmul  16732  pcid  16752  pcneg  16753  pc2dvds  16758  pcz  16760  pcaddlem  16767  pcadd  16768  pcmpt2  16772  pcbc  16779  qexpz  16780  expnprm  16781  sylow1lem1  19387  lspsneleq  20592  lspsneq  20599  lspfixed  20605  frlmsslss2  21197  chmatval  22194  chpmat1dlem  22200  chpdmatlem2  22204  ucncn  23653  ucnextcn  23672  ssblex  23797  prdsxmslem2  23901  ncvs1  24537  voliunlem1  24930  deg1mul3le  25497  deg1pw  25501  fta1blem  25549  bcmono  26641  dchrisum0flblem1  26872  dchrisum0flblem2  26873  pntibndlem1  26953  pntlemr  26966  nosupbnd1  27078  noinfbnd1  27093  noetalem1  27105  slerec  27180  finsumvtxdg2sstep  28539  umgr3cyclex  29169  nv1  29659  resf1o  31689  omndmul3  31963  symgcntz  31978  cycpmco2lem6  32022  tocyccntz  32035  rngurd  32107  measun  32850  measvuni  32853  measunl  32855  btwnconn1lem14  34714  segcon2  34719  seglelin  34730  neibastop3  34863  upixp  36217  fdc  36233  eqlkr3  37592  lkrshp  37596  lfl1dim  37612  lfl1dim2N  37613  eqlkr4  37656  2llnneN  37901  3dim2  37960  4atlem3  38088  4atlem11  38101  4atlem12  38104  pexmidlem4N  38465  lhp2at0nle  38527  lhple  38534  ltrnideq  38667  cdlemd9  38698  cdleme0ex2N  38716  cdleme0moN  38717  cdleme11a  38752  cdleme30a  38870  cdlemefs32sn1aw  38906  cdleme43fsv1snlem  38912  cdlemefs31fv1  38916  cdlemefs45eN  38923  cdleme41sn3a  38925  cdleme35h  38948  cdleme36a  38952  cdleme40m  38959  cdleme40n  38960  cdleme41sn3aw  38966  cdleme42h  38974  cdleme42k  38976  cdleme42mN  38979  cdleme43cN  38983  cdleme17d3  38988  cdleme48fvg  38992  cdlemeg47rv2  39002  cdlemeg46c  39005  cdlemeg46sfg  39012  cdlemeg46rjgN  39014  cdlemeg46rgv  39020  cdlemeg46req  39021  cdlemeg46gfv  39022  cdlemeg46gfre  39024  cdlemeg49lebilem  39031  cdleme50trn2  39043  cdlemg2kq  39094  cdlemb3  39098  cdlemg4f  39107  cdlemg9a  39124  cdlemg9b  39125  cdlemg9  39126  cdlemg11aq  39130  cdlemg12a  39135  cdlemg12b  39136  cdlemg12c  39137  cdlemg12d  39138  cdlemg12f  39140  cdlemg12g  39141  cdlemg12  39142  cdlemg13a  39143  cdlemg16  39149  cdlemg17e  39157  cdlemg17f  39158  cdlemg17g  39159  cdlemg17ir  39162  cdlemg17  39169  cdlemg18b  39171  cdlemg18c  39172  cdlemg33e  39202  trlcoabs2N  39214  trlcocnvat  39216  trlcolem  39218  trlco  39219  cdlemg44  39225  cdlemg47  39228  ltrncom  39230  tendococl  39264  tendoplcl  39273  tendoplcom  39274  tendoplass  39275  tendodi1  39276  tendodi2  39277  tendo0pl  39283  tendoipl  39289  cdlemh1  39307  cdlemi2  39311  tendo0mul  39318  tendo0mulr  39319  cdlemk2  39324  cdlemk3  39325  cdlemk4  39326  cdlemk6  39329  cdlemk8  39330  cdlemk12  39342  cdlemkole  39345  cdlemk14  39346  cdlemk15  39347  cdlemk5u  39353  cdlemk6u  39354  cdlemk12u  39364  cdlemkfid1N  39413  cdlemk19x  39435  cdlemk48  39442  cdlemk53a  39447  cdlemk56  39463  cdleml2N  39469  cdleml3N  39470  cdleml6  39473  cdleml7  39474  dva1dim  39477  dia2dimlem4  39559  dvhlveclem  39600  doca2N  39618  djajN  39629  cdlemn2a  39688  cdlemn3  39689  dihordlem6  39705  dihord5apre  39754  dihglbcpreN  39792  dihmeetcN  39794  dihmeetbN  39795  dihmeetlem10N  39808  dihmeetlem12N  39810  dihmeetlem15N  39813  dihmeetALTN  39819  dih1dimatlem0  39820  dihjatcclem3  39912  dihjatcclem4  39913  mapdpglem22  40185  hdmap14lem1a  40358  eldioph2b  41115  jm2.19lem4  41345  jm2.19  41346  jm2.26a  41353  jm2.26  41355  hbtlem2  41480  fnchoice  43308  stoweidlem42  44357  stoweidlem59  44374  fourierdlem42  44464
  Copyright terms: Public domain W3C validator