MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl211anc Structured version   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  12267  limsupbnd1  12268  limsupbnd2  12269  lbspss  16146  neiptopnei  17188  mbflimsup  19550  cxpneg  20564  cxpmul2  20572  cxpsqr  20586  cxpaddd  20600  cxpsubd  20601  divcxpd  20605  fsumharmonic  20842  bposlem1  21060  chpchtlim  21165  ax5seg  25869  lindff1  27258  islinds4  27273  modaddmulmod  28136  usgra2pthspth  28258  lshpnelb  29719  cdlemg2fv2  31334  cdlemg2m  31338  cdlemg9a  31366  cdlemg9b  31367  cdlemg12b  31378  cdlemg14f  31387  cdlemg14g  31388  cdlemg17dN  31397  cdlemkj  31597  cdlemkuv2  31601  cdlemk52  31688  cdlemk53a  31689
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