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

Theorem sylanbr 585
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 231 . 2 (𝜑𝜓)
3 sylanbr.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan 583 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  syl2anbr  602  funfv  6820  2mpo0  7476  tfrlem7  8143  omword  8322  isinf  8921  fsuppunbi  9036  axdc3lem2  10095  supsrlem  10755  expclzlem  13691  expgt0  13701  expge0  13704  expge1  13705  swrdnd2  14253  resqrex  14847  rplpwr  16152  4sqlem19  16549  gexcl3  19009  thlle  20692  decpmataa0  21697  neindisj  22046  ptcmplem5  22985  tsmsxplem1  23082  tsmsxplem2  23083  elovolmr  24405  itgsubst  24978  logeftb  25504  logbchbase  25686  legov  26708  unopbd  30128  nmcoplb  30143  nmcfnlb  30167  nmopcoi  30208  iocinif  30854  voliune  31941  signstfvneq0  32295  lfuhgr3  32825  nosupbnd1lem5  33686  noinfbnd1lem5  33701  f1omptsnlem  35281  unccur  35534  matunitlindflem2  35548  stoweidlem15  43277  hoiqssbllem3  43883  vonioo  43941  vonicc  43944  gboge9  44935  catprs  46011
  Copyright terms: Public domain W3C validator