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  disjiunOLD  4295  funfv  5770  tfrlem7  6854  omword  7021  isinf  7538  fsuppunbi  7653  axdc3lem2  8632  supsrlem  9290  expclzlem  11901  expgt0  11909  expge0  11912  expge1  11913  swrdvalodm2  12345  swrdvalodm  12346  resqrex  12752  rplpwr  13752  isprm2lem  13782  4sqlem19  14036  gexcl3  16098  thlle  18134  neindisj  18733  ptcmplem5  19640  tsmsxplem1  19739  tsmsxplem2  19740  elovolmr  20971  itgsubst  21533  logeftb  22044  constr2wlk  23509  unopbd  25431  nmcoplb  25446  nmcfnlb  25470  nmopcoi  25511  iocinif  26083  voliune  26657  signstfvneq0  26985  stoweidlem15  29822
  Copyright terms: Public domain W3C validator