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  2303  pm13.181  2521  rmob  3081  sspsstr  3283  disjne  3502  seex  4358  tron  4417  ordsucss  4611  ordsucelsuc  4615  xpcan2  5115  fssres  5410  funbrfvb  5567  funopfvb  5568  fvco  5597  fvimacnvi  5641  ffvresb  5692  funressn  5708  fvtp2  5727  fnex  5743  funex  5745  1st2nd  6168  frxp  6227  dftpos4  6255  tz7.48lem  6455  nnmsucr  6625  nnmcan  6634  xpmapenlem  7030  php  7047  php4  7050  omsucdomOLD  7058  isfinite2  7117  wofib  7262  r1limg  7445  r1pwcl  7521  cardmin2  7633  zornn0g  8134  intgru  8438  supsrlem  8735  uzindOLD  10108  fnn0ind  10113  uztrn2  10247  nnwo  10286  irradd  10342  qbtwnxr  10529  xltnegi  10545  xaddnemnf  10563  xaddnepnf  10564  xaddcom  10567  xnegdi  10570  elioore  10688  leexp2  11158  faclbnd  11305  faclbnd3  11307  dvdslelem  12575  divalglem1  12595  isprm2lem  12767  dvdsprime  12773  pcgcd  12932  cntri  14808  efgsrel  15045  xrsdsreclb  16420  znf1o  16507  restuni  16895  stoig  16896  restperf  16916  resstps  16919  pnfnei  16952  mnfnei  16953  cmpsublem  17128  tx1stc  17346  xkopt  17351  isfcls  17706  tgioo  18304  opnreen  18338  iscmet3  18721  dyaddisj  18953  limcmpt  19235  degltlem1  19460  ulmdvlem3  19781  lgsdi  20573  grpoidinvlem3  20875  ipasslem3  21413  spanuni  22125  5oalem3  22237  5oalem5  22239  mdslmd1lem2  22908  xaddeq0  23306  mptct  23347  mptctf  23350  esumcvg  23456  measres  23551  measdivcstOLD  23553  measdivcst  23554  probun  23624  eupath2lem3  23905  dfon2lem9  24149  noreson  24316  funpartfun  24483  cgrxfr  24680  segcon2  24730  brsegle2  24734  seglecgr12im  24735  segletr  24739  clfsebs  25358  trinv  25406  plimfil  25569  limfilnei  25572  cnegvex2  25671  rnegvex2  25672  clsmulrv  25694  nn0prpw  26250  connsubOLD  26265  comppfsc  26318  prtlem11  26745  mzpclall  26816  funbrafvb  28029  funopafvb  28030  afvco2  28048
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