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

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

Proof of Theorem syl211anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
31, 2jca 555 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl211anc.5 . 2 (((𝜓𝜒) ∧ 𝜃𝜏) → 𝜂)
73, 4, 5, 6syl3anc 1439 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  syl212anc  1449  syl221anc  1450  supicc  12434  modaddmulmod  12852  limsupgre  14332  limsupbnd1  14333  limsupbnd2  14334  lbspss  19205  lindff1  20282  islinds4  20297  mdetunilem9  20549  madutpos  20571  neiptopnei  21059  mbflimsup  23553  cxpneg  24547  cxpmul2  24555  cxpsqrt  24569  cxpaddd  24583  cxpsubd  24584  divcxpd  24588  fsumharmonic  24858  bposlem1  25129  lgsqr  25196  chpchtlim  25288  ax5seg  25938  archiabllem2c  29979  logdivsqrle  30958  lshpnelb  34691  cdlemg2fv2  36307  cdlemg2m  36311  cdlemg9a  36339  cdlemg9b  36340  cdlemg12b  36351  cdlemg14f  36360  cdlemg14g  36361  cdlemg17dN  36370  cdlemkj  36570  cdlemkuv2  36574  cdlemk52  36661  cdlemk53a  36662  mullimc  40268  mullimcf  40275  sfprmdvdsmersenne  41947  lincfsuppcl  42629
  Copyright terms: Public domain W3C validator