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

Theorem syl211anc 1329
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 554 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl211anc.5 . 2 (((𝜓𝜒) ∧ 𝜃𝜏) → 𝜂)
73, 4, 5, 6syl3anc 1323 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  syl212anc  1333  syl221anc  1334  supicc  12259  modaddmulmod  12674  limsupgre  14141  limsupbnd1  14142  limsupbnd2  14143  lbspss  18996  lindff1  20073  islinds4  20088  mdetunilem9  20340  madutpos  20362  neiptopnei  20841  mbflimsup  23334  cxpneg  24322  cxpmul2  24330  cxpsqrt  24344  cxpaddd  24358  cxpsubd  24359  divcxpd  24363  fsumharmonic  24633  bposlem1  24904  lgsqr  24971  chpchtlim  25063  ax5seg  25713  archiabllem2c  29526  lshpnelb  33737  cdlemg2fv2  35354  cdlemg2m  35358  cdlemg9a  35386  cdlemg9b  35387  cdlemg12b  35398  cdlemg14f  35407  cdlemg14g  35408  cdlemg17dN  35417  cdlemkj  35617  cdlemkuv2  35621  cdlemk52  35708  cdlemk53a  35709  mullimc  39239  mullimcf  39246  sfprmdvdsmersenne  40807  lincfsuppcl  41464
  Copyright terms: Public domain W3C validator