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  4014  funfv  5586  omword  6568  isinf  7076  axdc3lem2  8077  supsrlem  8733  expclzlem  11127  expgt0  11135  expge0  11138  expge1  11139  resqrex  11736  rplpwr  12735  isprm2lem  12765  4sqlem19  13010  gexcl3  14898  thlle  16597  neindisj  16854  ptcmplem5  17750  tsmsxplem1  17835  tsmsxplem2  17836  elovolmr  18835  itgsubst  19396  logeftb  19937  unopbd  22595  nmcoplb  22610  nmcfnlb  22634  nmopcoi  22675  iocinif  23274
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