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

Theorem sylanbr 473
Description: A syllogism inference. (Contributed by NM, 18-May-1994.)
Hypotheses
Ref Expression
sylanbr.1
sylanbr.2
Assertion
Ref Expression
sylanbr

Proof of Theorem sylanbr
StepHypRef Expression
1 sylanbr.1 . . 3
21biimpri 206 . 2
3 sylanbr.2 . 2
42, 3sylan 471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  syl2anbr  480  disjiunOLD  4443  funfv  5940  tfrlem7  7071  omword  7238  isinf  7753  fsuppunbi  7870  axdc3lem2  8852  supsrlem  9509  expclzlem  12190  expgt0  12199  expge0  12202  expge1  12203  swrdvalodm2  12664  swrdvalodm  12665  resqrex  13084  rplpwr  14194  isprm2lem  14224  4sqlem19  14481  gexcl3  16607  thlle  18728  decpmataa0  19269  neindisj  19618  ptcmplem5  20556  tsmsxplem1  20655  tsmsxplem2  20656  elovolmr  21887  itgsubst  22450  logeftb  22968  legov  23972  constr2wlk  24600  unopbd  26934  nmcoplb  26949  nmcfnlb  26973  nmopcoi  27014  iocinif  27592  voliune  28201  signstfvneq0  28529  stoweidlem15  31797
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
  Copyright terms: Public domain W3C validator