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

Theorem sylanbr 473
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 471 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 371
This theorem is referenced by:  syl2anbr  480  funfv  5940  tfrlem7  7070  omword  7237  isinf  7752  fsuppunbi  7868  axdc3lem2  8848  supsrlem  9505  expclzlem  12193  expgt0  12202  expge0  12205  expge1  12206  swrdnd2  12669  resqrex  13096  rplpwr  14206  isprm2lem  14236  4sqlem19  14493  gexcl3  16734  thlle  18855  decpmataa0  19396  neindisj  19745  ptcmplem5  20682  tsmsxplem1  20781  tsmsxplem2  20782  elovolmr  22013  itgsubst  22576  logeftb  23094  legov  24098  constr2wlk  24727  unopbd  27061  nmcoplb  27076  nmcfnlb  27100  nmopcoi  27141  iocinif  27752  voliune  28374  signstfvneq0  28726  stoweidlem15  32000
  Copyright terms: Public domain W3C validator