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

Theorem sylanb 458
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 186 . 2  |-  ( ph  ->  ps )
3 sylanb.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 457 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  syl2anb  465  anabsan  786  eqtr2  2301  pm13.181  2519  rmob  3079  sspsstr  3281  disjne  3500  seex  4356  tron  4415  ordsucss  4609  ordsucelsuc  4613  xpcan2  5113  fssres  5408  funbrfvb  5565  funopfvb  5566  fvco  5595  fvimacnvi  5639  ffvresb  5690  funressn  5706  fvtp2  5725  fnex  5741  funex  5743  1st2nd  6166  frxp  6225  dftpos4  6253  tz7.48lem  6453  nnmsucr  6623  nnmcan  6632  xpmapenlem  7028  php  7045  php4  7048  omsucdomOLD  7056  isfinite2  7115  wofib  7260  r1limg  7443  r1pwcl  7519  cardmin2  7631  zornn0g  8132  intgru  8436  supsrlem  8733  uzindOLD  10106  fnn0ind  10111  uztrn2  10245  nnwo  10284  irradd  10340  qbtwnxr  10527  xltnegi  10543  xaddnemnf  10561  xaddnepnf  10562  xaddcom  10565  xnegdi  10568  elioore  10686  leexp2  11156  faclbnd  11303  faclbnd3  11305  dvdslelem  12573  divalglem1  12593  isprm2lem  12765  dvdsprime  12771  pcgcd  12930  cntri  14806  efgsrel  15043  xrsdsreclb  16418  znf1o  16505  restuni  16893  stoig  16894  restperf  16914  resstps  16917  pnfnei  16950  mnfnei  16951  cmpsublem  17126  tx1stc  17344  xkopt  17349  isfcls  17704  tgioo  18302  opnreen  18336  iscmet3  18719  dyaddisj  18951  limcmpt  19233  degltlem1  19458  ulmdvlem3  19779  lgsdi  20571  grpoidinvlem3  20873  ipasslem3  21411  spanuni  22123  5oalem3  22235  5oalem5  22237  mdslmd1lem2  22906  eupath2lem3  23314  dfon2lem9  23558  noreson  23725  funpartfun  23892  cgrxfr  24089  segcon2  24139  brsegle2  24143  seglecgr12im  24144  segletr  24148  clfsebs  24759  trinv  24807  plimfil  24970  limfilnei  24973  cnegvex2  25072  rnegvex2  25073  clsmulrv  25095  nn0prpw  25651  connsubOLD  25666  comppfsc  25719  prtlem11  26146  mzpclall  26217  funbrafvb  27430  funopafvb  27431  afvco2  27449
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 177  df-an 360
  Copyright terms: Public domain W3C validator