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

Theorem syl211anc 1190
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 519 . 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 1184 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  syl212anc  1194  syl221anc  1195  limsupgre  12203  limsupbnd1  12204  limsupbnd2  12205  lbspss  16082  neiptopnei  17120  mbflimsup  19426  cxpneg  20440  cxpmul2  20448  cxpsqr  20462  cxpaddd  20476  cxpsubd  20477  divcxpd  20481  fsumharmonic  20718  bposlem1  20936  chpchtlim  21041  ax5seg  25592  lindff1  26960  islinds4  26975  lshpnelb  29100  cdlemg2fv2  30715  cdlemg2m  30719  cdlemg9a  30747  cdlemg9b  30748  cdlemg12b  30759  cdlemg14f  30768  cdlemg14g  30769  cdlemg17dN  30778  cdlemkj  30978  cdlemkuv2  30982  cdlemk52  31069  cdlemk53a  31070
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator