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

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

Proof of Theorem sylanbr
StepHypRef Expression
1 sylanbr.1 . . 3  |-  ( ps  <->  ph )
21biimpri 206 . 2  |-  ( ph  ->  ps )
3 sylanbr.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 469 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  syl2anbr  478  funfv  5916  tfrlem7  7086  omword  7256  isinf  7768  fsuppunbi  7884  axdc3lem2  8863  supsrlem  9518  expclzlem  12234  expgt0  12243  expge0  12246  expge1  12247  swrdnd2  12714  resqrex  13233  rplpwr  14403  isprm2lem  14433  4sqlem19  14690  gexcl3  16931  thlle  19026  decpmataa0  19561  neindisj  19911  ptcmplem5  20848  tsmsxplem1  20947  tsmsxplem2  20948  elovolmr  22179  itgsubst  22742  logeftb  23263  logbchbase  23438  legov  24355  constr2wlk  25017  unopbd  27347  nmcoplb  27362  nmcfnlb  27386  nmopcoi  27427  iocinif  28040  voliune  28678  signstfvneq0  29035  f1omptsnlem  31252  stoweidlem15  37165  gboage9  37818
  Copyright terms: Public domain W3C validator