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

Theorem sylanbr 460
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 198 . 2  |-  ( ph  ->  ps )
3 sylanbr.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 458 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  syl2anbr  467  disjiunOLD  4167  funfv  5753  omword  6776  isinf  7285  axdc3lem2  8291  supsrlem  8946  expclzlem  11364  expgt0  11372  expge0  11375  expge1  11376  resqrex  12015  rplpwr  13015  isprm2lem  13045  4sqlem19  13290  gexcl3  15180  thlle  16883  neindisj  17140  ptcmplem5  18044  tsmsxplem1  18139  tsmsxplem2  18140  elovolmr  19329  itgsubst  19890  logeftb  20435  constr2wlk  21555  unopbd  23475  nmcoplb  23490  nmcfnlb  23514  nmopcoi  23555  iocinif  24101  voliune  24542  stoweidlem15  27635
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 178  df-an 361
  Copyright terms: Public domain W3C validator