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

Theorem sylanb 474
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 197 . 2  |-  ( ph  ->  ps )
3 sylanb.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 473 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  syl2anb  481  anabsan  820  eqtr2  2456  pm13.181  2743  rmob  3397  sspsstr  3576  disjne  3844  seex  4817  xpcan2  5294  tron  5465  fssres  5766  funbrfvb  5923  funopfvb  5924  fvco  5957  fvimacnvi  6011  ffvresb  6069  funressn  6092  funresdfunsn  6121  fvtp2  6127  fvtp2g  6130  fnex  6147  funex  6148  ordsucss  6659  ordsucelsuc  6663  1st2nd  6853  frxp  6917  dftpos4  7000  tz7.48lem  7166  nnmsucr  7334  nnmcan  7343  xpmapenlem  7745  php  7762  php4  7765  isfinite2  7835  fundmfibi  7861  fiinfcl  8017  wofib  8060  r1limg  8241  r1pwcl  8317  cardmin2  8431  zornn0g  8933  intgru  9238  supsrlem  9534  fnn0ind  11034  uztrn2  11176  nnwo  11224  irradd  11288  qbtwnxr  11493  xltnegi  11509  xaddnemnf  11527  xaddnepnf  11528  xaddcom  11531  xnegdi  11534  elioore  11666  uzsubsubfz1  11820  fzo1fzo0n0  11955  elfzonelfzo  12008  leexp2  12324  faclbnd  12472  faclbnd3  12474  brfi1uzind  12641  swrdccat3b  12837  dvdslelem  14327  divalglem1  14350  isprm2lem  14593  dvdsprime  14599  pcgcd  14781  cntri  16926  efgsrel  17310  xrsdsreclb  18941  znf1o  19044  restuni  20100  stoig  20101  restperf  20122  resstps  20125  pnfnei  20158  mnfnei  20159  cnnei  20220  cmpsublem  20336  comppfsc  20469  tx1stc  20587  xkopt  20592  isfcls  20946  tgioo  21716  opnreen  21751  iscmet3  22147  dyaddisj  22422  limcmpt  22706  degltlem1  22889  ulmdvlem3  23213  lgsdi  24114  clwlkfclwwlk  25408  2wlkonotv  25441  eupath2lem3  25543  grpoidinvlem3  25770  ipasslem3  26310  spanuni  27023  5oalem3  27135  5oalem5  27137  mdslmd1lem2  27805  mptct  28136  mptctf  28139  xaddeq0  28164  ordtconlem1  28560  esumcvg  28737  ldgenpisyslem1  28815  measres  28874  measdivcstOLD  28876  measdivcst  28877  probun  29069  elmpps  29990  dfon2lem9  30215  noreson  30325  funpartfun  30486  cgrxfr  30598  segcon2  30648  brsegle2  30652  seglecgr12im  30653  segletr  30657  nn0prpw  30755  bj-seex  31267  ptrecube  31634  poimirlem28  31662  ftc1anclem5  31715  ftc1anc  31719  exlimddvfi  32056  prtlem11  32136  mzpclall  35268  4an31  36481  iundjiun  37797  funbrafvb  38038  funopafvb  38039  afvco2  38058  usgfis  38506  usgfisALT  38510
  Copyright terms: Public domain W3C validator