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

Theorem syl211anc 1488
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 503 . 2 (𝜑 → (𝜓𝜒))
4 syl3anc.3 . 2 (𝜑𝜃)
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl211anc.5 . 2 (((𝜓𝜒) ∧ 𝜃𝜏) → 𝜂)
73, 4, 5, 6syl3anc 1483 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  syl212anc  1492  syl221anc  1493  supicc  12543  modaddmulmod  12961  limsupgre  14435  limsupbnd1  14436  limsupbnd2  14437  lbspss  19289  lindff1  20369  islinds4  20384  mdetunilem9  20637  madutpos  20659  neiptopnei  21150  mbflimsup  23647  cxpneg  24641  cxpmul2  24649  cxpsqrt  24663  cxpaddd  24677  cxpsubd  24678  divcxpd  24682  fsumharmonic  24952  bposlem1  25223  lgsqr  25290  chpchtlim  25382  ax5seg  26032  archiabllem2c  30074  logdivsqrle  31053  lshpnelb  34764  cdlemg2fv2  36381  cdlemg2m  36385  cdlemg9a  36413  cdlemg9b  36414  cdlemg12b  36425  cdlemg14f  36434  cdlemg14g  36435  cdlemg17dN  36444  cdlemkj  36644  cdlemkuv2  36648  cdlemk52  36735  cdlemk53a  36736  mullimc  40328  mullimcf  40335  sfprmdvdsmersenne  42095  lincfsuppcl  42770
  Copyright terms: Public domain W3C validator