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  11955  limsupbnd1  11956  limsupbnd2  11957  lbspss  15835  mbflimsup  19021  cxpneg  20028  cxpmul2  20036  cxpsqr  20050  cxpaddd  20064  cxpsubd  20065  divcxpd  20069  fsumharmonic  20305  bposlem1  20523  chpchtlim  20628  ax5seg  24566  islimrs4  25582  lindff1  27290  islinds4  27305  lshpnelb  29174  cdlemg2fv2  30789  cdlemg2m  30793  cdlemg9a  30821  cdlemg9b  30822  cdlemg12b  30833  cdlemg14f  30842  cdlemg14g  30843  cdlemg17dN  30852  cdlemkj  31052  cdlemkuv2  31056  cdlemk52  31143  cdlemk53a  31144
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