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

Theorem syl211anc 1225
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 1219 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  1229  syl221anc  1230  supicc  11553  modaddmulmod  11885  limsupgre  13080  limsupbnd1  13081  limsupbnd2  13082  lbspss  17289  lindff1  18377  islinds4  18392  mdetunilem9  18561  madutpos  18583  neiptopnei  18871  mbflimsup  21280  cxpneg  22262  cxpmul2  22270  cxpsqr  22284  cxpaddd  22298  cxpsubd  22299  divcxpd  22303  fsumharmonic  22541  bposlem1  22759  chpchtlim  22864  ax5seg  23356  usgra2pthspth  30463  lincfsuppcl  31099  lshpnelb  32987  cdlemg2fv2  34602  cdlemg2m  34606  cdlemg9a  34634  cdlemg9b  34635  cdlemg12b  34646  cdlemg14f  34655  cdlemg14g  34656  cdlemg17dN  34665  cdlemkj  34865  cdlemkuv2  34869  cdlemk52  34956  cdlemk53a  34957
  Copyright terms: Public domain W3C validator