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  6252  2mpt20  6867  tfrlem7  7464  omword  7635  isinf  8158  fsuppunbi  8281  axdc3lem2  9258  supsrlem  9917  expclzlem  12867  expgt0  12876  expge0  12879  expge1  12880  swrdnd2  13415  resqrex  13972  rplpwr  15257  isprm2lem  15375  4sqlem19  15648  gexcl3  17983  thlle  20022  decpmataa0  20554  neindisj  20902  ptcmplem5  21841  tsmsxplem1  21937  tsmsxplem2  21938  elovolmr  23225  itgsubst  23793  logeftb  24311  logbchbase  24490  legov  25461  unopbd  28844  nmcoplb  28859  nmcfnlb  28883  nmopcoi  28924  iocinif  29517  voliune  30266  signstfvneq0  30623  nosupbnd1lem5  31832  f1omptsnlem  33154  unccur  33363  matunitlindflem2  33377  stoweidlem15  39995  hoiqssbllem3  40601  vonioo  40659  vonicc  40662  gboge9  41417
  Copyright terms: Public domain W3C validator