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

Theorem sylanbr 490
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 218 . 2 (𝜑𝜓)
3 sylanbr.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan 488 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  syl2anbr  497  funfv  6222  2mpt20  6835  tfrlem7  7424  omword  7595  isinf  8117  fsuppunbi  8240  axdc3lem2  9217  supsrlem  9876  expclzlem  12824  expgt0  12833  expge0  12836  expge1  12837  swrdnd2  13371  resqrex  13925  rplpwr  15200  isprm2lem  15318  4sqlem19  15591  gexcl3  17923  thlle  19960  decpmataa0  20492  neindisj  20831  ptcmplem5  21770  tsmsxplem1  21866  tsmsxplem2  21867  elovolmr  23151  itgsubst  23716  logeftb  24234  logbchbase  24409  legov  25380  unopbd  28720  nmcoplb  28735  nmcfnlb  28759  nmopcoi  28800  iocinif  29384  voliune  30070  signstfvneq0  30426  f1omptsnlem  32812  unccur  33021  matunitlindflem2  33035  stoweidlem15  39536  hoiqssbllem3  40142  vonioo  40200  vonicc  40203  gboage9  40944
  Copyright terms: Public domain W3C validator