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

Theorem sylanbr 583
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 227 . 2 (𝜑𝜓)
3 sylanbr.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan 581 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  syl2anbr  600  rspc4v  3597  funfv  6932  2mpo0  7606  tfrlem7  8333  omword  8521  isinf  9210  isinfOLD  9211  fsuppunbi  9334  axdc3lem2  10395  supsrlem  11055  expclzlem  13998  expgt0  14010  expge0  14013  expge1  14014  swrdnd2  14552  resqrex  15144  rplpwr  16446  4sqlem19  16843  gexcl3  19377  thlle  21125  thlleOLD  21126  decpmataa0  22140  neindisj  22491  ptcmplem5  23430  tsmsxplem1  23527  tsmsxplem2  23528  elovolmr  24863  itgsubst  25436  logeftb  25962  logbchbase  26144  nosupbnd1lem5  27083  noinfbnd1lem5  27098  legov  27576  unopbd  31006  nmcoplb  31021  nmcfnlb  31045  nmopcoi  31086  iocinif  31738  voliune  32892  signstfvneq0  33248  lfuhgr3  33777  f1omptsnlem  35857  unccur  36111  matunitlindflem2  36125  stoweidlem15  44346  hoiqssbllem3  44955  vonioo  45013  vonicc  45016  gboge9  46046  catprs  47121
  Copyright terms: Public domain W3C validator