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

Theorem syl211anc 1373
 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 515 . 2 (𝜑 → (𝜓𝜒))
4 syl3anc.3 . 2 (𝜑𝜃)
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl211anc.5 . 2 (((𝜓𝜒) ∧ 𝜃𝜏) → 𝜂)
73, 4, 5, 6syl3anc 1368 1 (𝜑𝜂)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  syl212anc  1377  syl221anc  1378  supicc  12899  modaddmulmod  13321  limsupgre  14850  limsupbnd1  14851  limsupbnd2  14852  lbspss  19868  lindff1  20531  islinds4  20546  mdetunilem9  21266  madutpos  21288  neiptopnei  21778  mbflimsup  24311  cxpneg  25316  cxpmul2  25324  cxpsqrt  25338  cxpaddd  25352  cxpsubd  25353  divcxpd  25357  fsumharmonic  25641  bposlem1  25912  lgsqr  25979  chpchtlim  26107  ax5seg  26776  archiabllem2c  30923  qsidomlem2  31098  logdivsqrle  32097  frrlem15  33325  lindsadd  35201  lshpnelb  36431  cdlemg2fv2  38047  cdlemg2m  38051  cdlemg9a  38079  cdlemg9b  38080  cdlemg12b  38091  cdlemg14f  38100  cdlemg14g  38101  cdlemg17dN  38110  cdlemkj  38310  cdlemkuv2  38314  cdlemk52  38401  cdlemk53a  38402  mullimc  42426  mullimcf  42433  sfprmdvdsmersenne  44289  lincfsuppcl  44988
 Copyright terms: Public domain W3C validator