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

Theorem syl211anc 1413
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 1407 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  1417  syl221anc  1418  supicc  12402  modaddmulmod  12820  limsupgre  14300  limsupbnd1  14301  limsupbnd2  14302  lbspss  19173  lindff1  20250  islinds4  20265  mdetunilem9  20517  madutpos  20539  neiptopnei  21027  mbflimsup  23521  cxpneg  24515  cxpmul2  24523  cxpsqrt  24537  cxpaddd  24551  cxpsubd  24552  divcxpd  24556  fsumharmonic  24826  bposlem1  25097  lgsqr  25164  chpchtlim  25256  ax5seg  25906  archiabllem2c  29947  logdivsqrle  30926  lshpnelb  34659  cdlemg2fv2  36275  cdlemg2m  36279  cdlemg9a  36307  cdlemg9b  36308  cdlemg12b  36319  cdlemg14f  36328  cdlemg14g  36329  cdlemg17dN  36338  cdlemkj  36538  cdlemkuv2  36542  cdlemk52  36629  cdlemk53a  36630  mullimc  40236  mullimcf  40243  sfprmdvdsmersenne  41915  lincfsuppcl  42597
  Copyright terms: Public domain W3C validator