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

Theorem syl211anc 1232
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 530 . 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 1226 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  syl212anc  1236  syl221anc  1237  supicc  11671  modaddmulmod  12035  limsupgre  13386  limsupbnd1  13387  limsupbnd2  13388  lbspss  17923  lindff1  19022  islinds4  19037  mdetunilem9  19289  madutpos  19311  neiptopnei  19800  mbflimsup  22239  cxpneg  23230  cxpmul2  23238  cxpsqrt  23252  cxpaddd  23266  cxpsubd  23267  divcxpd  23271  fsumharmonic  23539  bposlem1  23757  chpchtlim  23862  ax5seg  24443  archiabllem2c  27973  mullimc  31861  mullimcf  31868  usgra2pthspth  32723  lincfsuppcl  33268  lshpnelb  35106  cdlemg2fv2  36723  cdlemg2m  36727  cdlemg9a  36755  cdlemg9b  36756  cdlemg12b  36767  cdlemg14f  36776  cdlemg14g  36777  cdlemg17dN  36786  cdlemkj  36986  cdlemkuv2  36990  cdlemk52  37077  cdlemk53a  37078
  Copyright terms: Public domain W3C validator