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

Theorem sylanbr 461
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 199 . 2  |-  ( ph  ->  ps )
3 sylanbr.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 459 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  syl2anbr  468  disjiunOLD  4206  funfv  5793  omword  6816  isinf  7325  axdc3lem2  8336  supsrlem  8991  expclzlem  11410  expgt0  11418  expge0  11421  expge1  11422  resqrex  12061  rplpwr  13061  isprm2lem  13091  4sqlem19  13336  gexcl3  15226  thlle  16929  neindisj  17186  ptcmplem5  18092  tsmsxplem1  18187  tsmsxplem2  18188  elovolmr  19377  itgsubst  19938  logeftb  20483  constr2wlk  21603  unopbd  23523  nmcoplb  23538  nmcfnlb  23562  nmopcoi  23603  iocinif  24149  voliune  24590  stoweidlem15  27754  swrdvalodm2  28222  swrdvalodm  28223
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 179  df-an 362
  Copyright terms: Public domain W3C validator