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

Theorem sylanb 459
Description: A syllogism inference. (Contributed by NM, 18-May-1994.)
Hypotheses
Ref Expression
sylanb.1  |-  ( ph  <->  ps )
sylanb.2  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
sylanb  |-  ( (
ph  /\  ch )  ->  th )

Proof of Theorem sylanb
StepHypRef Expression
1 sylanb.1 . . 3  |-  ( ph  <->  ps )
21biimpi 187 . 2  |-  ( ph  ->  ps )
3 sylanb.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 458 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  syl2anb  466  anabsan  787  eqtr2  2453  pm13.181  2671  rmob  3241  sspsstr  3444  disjne  3665  seex  4537  tron  4596  ordsucss  4790  ordsucelsuc  4794  xpcan2  5298  fssres  5602  funbrfvb  5761  funopfvb  5762  fvco  5791  fvimacnvi  5836  ffvresb  5892  funressn  5911  fvtp2  5932  fvtp2g  5935  fnex  5953  funex  5955  1st2nd  6385  frxp  6448  dftpos4  6490  tz7.48lem  6690  nnmsucr  6860  nnmcan  6869  xpmapenlem  7266  php  7283  php4  7286  omsucdomOLD  7294  isfinite2  7357  wofib  7506  r1limg  7689  r1pwcl  7765  cardmin2  7877  zornn0g  8377  intgru  8681  supsrlem  8978  uzindOLD  10356  fnn0ind  10361  uztrn2  10495  nnwo  10534  irradd  10590  qbtwnxr  10778  xltnegi  10794  xaddnemnf  10812  xaddnepnf  10813  xaddcom  10816  xnegdi  10819  elioore  10938  leexp2  11426  faclbnd  11573  faclbnd3  11575  brfi1uzind  11707  dvdslelem  12886  divalglem1  12906  isprm2lem  13078  dvdsprime  13084  pcgcd  13243  cntri  15121  efgsrel  15358  xrsdsreclb  16737  znf1o  16824  restuni  17218  stoig  17219  restperf  17240  resstps  17243  pnfnei  17276  mnfnei  17277  cnnei  17338  cmpsublem  17454  tx1stc  17674  xkopt  17679  isfcls  18033  tgioo  18819  opnreen  18854  iscmet3  19238  dyaddisj  19480  limcmpt  19762  degltlem1  19987  ulmdvlem3  20310  lgsdi  21108  eupath2lem3  21693  grpoidinvlem3  21786  ipasslem3  22326  spanuni  23038  5oalem3  23150  5oalem5  23152  mdslmd1lem2  23821  mptct  24101  mptctf  24104  xaddeq0  24111  esumcvg  24468  measres  24568  measdivcstOLD  24570  measdivcst  24571  probun  24669  dfon2lem9  25410  noreson  25607  funpartfun  25780  cgrxfr  25981  segcon2  26031  brsegle2  26035  seglecgr12im  26036  segletr  26040  ftc1anclem5  26274  ftc1anc  26278  nn0prpw  26317  comppfsc  26378  prtlem11  26706  mzpclall  26775  funbrafvb  27987  funopafvb  27988  afvco2  28007  fzo1fzo0n0  28111  elfzonelfzo  28115  swrdccat3b  28185  2wlkonotv  28297
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
  Copyright terms: Public domain W3C validator