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

Theorem sylanbr 459
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 197 . 2  |-  ( ph  ->  ps )
3 sylanbr.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:  syl2anbr  466  disjiunOLD  4095  funfv  5669  omword  6655  isinf  7164  axdc3lem2  8167  supsrlem  8823  expclzlem  11220  expgt0  11228  expge0  11231  expge1  11232  resqrex  11832  rplpwr  12832  isprm2lem  12862  4sqlem19  13107  gexcl3  14997  thlle  16703  neindisj  16960  ptcmplem5  17852  tsmsxplem1  17937  tsmsxplem2  17938  elovolmr  18939  itgsubst  19500  logeftb  20045  unopbd  22709  nmcoplb  22724  nmcfnlb  22748  nmopcoi  22789  iocinif  23346
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