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

Theorem syl211anc 1270
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 534 . 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 1264 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  syl212anc  1274  syl221anc  1275  supicc  11778  modaddmulmod  12153  limsupgre  13520  limsupgreOLD  13521  limsupbnd1  13522  limsupbnd1OLD  13523  limsupbnd2  13524  limsupbnd2OLD  13525  lbspss  18240  lindff1  19309  islinds4  19324  mdetunilem9  19576  madutpos  19598  neiptopnei  20079  mbflimsup  22500  mbflimsupOLD  22501  cxpneg  23491  cxpmul2  23499  cxpsqrt  23513  cxpaddd  23527  cxpsubd  23528  divcxpd  23532  fsumharmonic  23802  bposlem1  24075  chpchtlim  24180  ax5seg  24814  archiabllem2c  28350  lshpnelb  32259  cdlemg2fv2  33876  cdlemg2m  33880  cdlemg9a  33908  cdlemg9b  33909  cdlemg12b  33920  cdlemg14f  33929  cdlemg14g  33930  cdlemg17dN  33939  cdlemkj  34139  cdlemkuv2  34143  cdlemk52  34230  cdlemk53a  34231  mullimc  37268  mullimcf  37275  usgra2pthspth  38430  lincfsuppcl  38975
  Copyright terms: Public domain W3C validator