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

Theorem syl211anc 1188
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
syl211anc.5  |-  ( ( ( ps  /\  ch )  /\  th  /\  ta )  ->  et )
Assertion
Ref Expression
syl211anc  |-  ( ph  ->  et )

Proof of Theorem syl211anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 518 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 sylXanc.3 . 2  |-  ( ph  ->  th )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl211anc.5 . 2  |-  ( ( ( ps  /\  ch )  /\  th  /\  ta )  ->  et )
73, 4, 5, 6syl3anc 1182 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  syl212anc  1192  syl221anc  1193  limsupgre  11971  limsupbnd1  11972  limsupbnd2  11973  lbspss  15851  mbflimsup  19037  cxpneg  20044  cxpmul2  20052  cxpsqr  20066  cxpaddd  20080  cxpsubd  20081  divcxpd  20085  fsumharmonic  20321  bposlem1  20539  chpchtlim  20644  ax5seg  24638  islimrs4  25685  lindff1  27393  islinds4  27408  lshpnelb  29796  cdlemg2fv2  31411  cdlemg2m  31415  cdlemg9a  31443  cdlemg9b  31444  cdlemg12b  31455  cdlemg14f  31464  cdlemg14g  31465  cdlemg17dN  31474  cdlemkj  31674  cdlemkuv2  31678  cdlemk52  31765  cdlemk53a  31766
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator