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

Theorem syl211anc 1377
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl211anc.5 (((𝜓𝜒) ∧ 𝜃𝜏) → 𝜂)
Assertion
Ref Expression
syl211anc (𝜑𝜂)

Proof of Theorem syl211anc
StepHypRef Expression
1 syl3anc.1 . . 3 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
31, 2jca 513 . 2 (𝜑 → (𝜓𝜒))
4 syl3anc.3 . 2 (𝜑𝜃)
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl211anc.5 . 2 (((𝜓𝜒) ∧ 𝜃𝜏) → 𝜂)
73, 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:  syl212anc  1381  syl221anc  1382  frrlem15  9747  supicc  13473  modaddmulmod  13898  limsupgre  15420  limsupbnd1  15421  limsupbnd2  15422  lbspss  20680  lindff1  21358  islinds4  21373  mdetunilem9  22103  madutpos  22125  neiptopnei  22617  mbflimsup  25164  cxpneg  26170  cxpmul2  26178  cxpsqrt  26192  cxpaddd  26206  cxpsubd  26207  divcxpd  26211  fsumharmonic  26495  bposlem1  26766  lgsqr  26833  chpchtlim  26961  sltmul2d  27603  ax5seg  28175  archiabllem2c  32318  qsidomlem2  32529  logdivsqrle  33599  lindsadd  36418  lshpnelb  37791  cdlemg2fv2  39408  cdlemg2m  39412  cdlemg9a  39440  cdlemg9b  39441  cdlemg12b  39452  cdlemg14f  39461  cdlemg14g  39462  cdlemg17dN  39471  cdlemkj  39671  cdlemkuv2  39675  cdlemk52  39762  cdlemk53a  39763  mullimc  44266  mullimcf  44273  sfprmdvdsmersenne  46205  lincfsuppcl  46995
  Copyright terms: Public domain W3C validator