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

Theorem sylanbr 571
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 569 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382
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 383
This theorem is referenced by:  syl2anbr  586  funfv  6407  2mpt20  7029  tfrlem7  7632  omword  7804  isinf  8329  fsuppunbi  8452  axdc3lem2  9475  supsrlem  10134  expclzlem  13091  expgt0  13100  expge0  13103  expge1  13104  swrdnd2  13642  resqrex  14199  rplpwr  15484  4sqlem19  15874  gexcl3  18209  thlle  20258  decpmataa0  20793  neindisj  21142  ptcmplem5  22080  tsmsxplem1  22176  tsmsxplem2  22177  elovolmr  23464  itgsubst  24032  logeftb  24551  logbchbase  24730  legov  25701  unopbd  29214  nmcoplb  29229  nmcfnlb  29253  nmopcoi  29294  iocinif  29883  voliune  30632  signstfvneq0  30989  nosupbnd1lem5  32195  f1omptsnlem  33520  unccur  33725  matunitlindflem2  33739  stoweidlem15  40749  hoiqssbllem3  41358  vonioo  41416  vonicc  41419  gboge9  42180
  Copyright terms: Public domain W3C validator