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

Theorem sylanbr 577
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 220 . 2 (𝜑𝜓)
3 sylanbr.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan 575 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386
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 199  df-an 387
This theorem is referenced by:  syl2anbr  592  funfv  6525  2mpt20  7159  tfrlem7  7762  omword  7934  isinf  8461  fsuppunbi  8584  axdc3lem2  9608  supsrlem  10268  expclzlem  13202  expgt0  13211  expge0  13214  expge1  13215  swrdnd2  13750  resqrex  14398  rplpwr  15682  4sqlem19  16071  gexcl3  18386  thlle  20440  decpmataa0  20980  neindisj  21329  ptcmplem5  22268  tsmsxplem1  22364  tsmsxplem2  22365  elovolmr  23680  itgsubst  24249  logeftb  24767  logbchbase  24949  legov  25936  unopbd  29446  nmcoplb  29461  nmcfnlb  29485  nmopcoi  29526  iocinif  30107  voliune  30890  signstfvneq0  31250  nosupbnd1lem5  32447  f1omptsnlem  33779  unccur  34019  matunitlindflem2  34034  stoweidlem15  41163  hoiqssbllem3  41769  vonioo  41827  vonicc  41830  gboge9  42681
  Copyright terms: Public domain W3C validator