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

Theorem syl211anc 1368
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 512 . 2 (𝜑 → (𝜓𝜒))
4 syl3anc.3 . 2 (𝜑𝜃)
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl211anc.5 . 2 (((𝜓𝜒) ∧ 𝜃𝜏) → 𝜂)
73, 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:  syl212anc  1372  syl221anc  1373  supicc  12874  modaddmulmod  13294  limsupgre  14826  limsupbnd1  14827  limsupbnd2  14828  lbspss  19783  lindff1  20892  islinds4  20907  mdetunilem9  21157  madutpos  21179  neiptopnei  21668  mbflimsup  24194  cxpneg  25191  cxpmul2  25199  cxpsqrt  25213  cxpaddd  25227  cxpsubd  25228  divcxpd  25232  fsumharmonic  25516  bposlem1  25787  lgsqr  25854  chpchtlim  25982  ax5seg  26651  archiabllem2c  30751  qsidomlem2  30883  logdivsqrle  31820  frrlem15  33039  lindsadd  34766  lshpnelb  36000  cdlemg2fv2  37616  cdlemg2m  37620  cdlemg9a  37648  cdlemg9b  37649  cdlemg12b  37660  cdlemg14f  37669  cdlemg14g  37670  cdlemg17dN  37679  cdlemkj  37879  cdlemkuv2  37883  cdlemk52  37970  cdlemk53a  37971  mullimc  41773  mullimcf  41780  sfprmdvdsmersenne  43645  lincfsuppcl  44396
  Copyright terms: Public domain W3C validator