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

Theorem sylanbr 489
 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 217 . 2 (𝜑𝜓)
3 sylanbr.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan 487 1 ((𝜑𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  syl2anbr  496  funfv  6175  2mpt20  6780  tfrlem7  7366  omword  7537  isinf  8058  fsuppunbi  8179  axdc3lem2  9156  supsrlem  9811  expclzlem  12746  expgt0  12755  expge0  12758  expge1  12759  swrdnd2  13285  resqrex  13839  rplpwr  15114  isprm2lem  15232  4sqlem19  15505  gexcl3  17825  thlle  19860  decpmataa0  20392  neindisj  20731  ptcmplem5  21670  tsmsxplem1  21766  tsmsxplem2  21767  elovolmr  23051  itgsubst  23616  logeftb  24134  logbchbase  24309  legov  25280  constr2wlk  26128  unopbd  28258  nmcoplb  28273  nmcfnlb  28297  nmopcoi  28338  iocinif  28933  voliune  29619  signstfvneq0  29975  f1omptsnlem  32359  unccur  32562  matunitlindflem2  32576  stoweidlem15  38908  hoiqssbllem3  39514  vonioo  39573  vonicc  39576  gboage9  40186
 Copyright terms: Public domain W3C validator