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

Theorem syl211anc 1224
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 532 . 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 1218 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  syl212anc  1228  syl221anc  1229  supicc  11425  modaddmulmod  11757  limsupgre  12951  limsupbnd1  12952  limsupbnd2  12953  lbspss  17140  lindff1  18224  islinds4  18239  mdetunilem9  18401  madutpos  18423  neiptopnei  18711  mbflimsup  21119  cxpneg  22101  cxpmul2  22109  cxpsqr  22123  cxpaddd  22137  cxpsubd  22138  divcxpd  22142  fsumharmonic  22380  bposlem1  22598  chpchtlim  22703  ax5seg  23135  usgra2pthspth  30248  lincfsuppcl  30836  lshpnelb  32469  cdlemg2fv2  34084  cdlemg2m  34088  cdlemg9a  34116  cdlemg9b  34117  cdlemg12b  34128  cdlemg14f  34137  cdlemg14g  34138  cdlemg17dN  34147  cdlemkj  34347  cdlemkuv2  34351  cdlemk52  34438  cdlemk53a  34439
  Copyright terms: Public domain W3C validator