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

Theorem sylanbr 491
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 489 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 385
This theorem is referenced by:  syl2anbr  498  funfv  6427  2mpt20  7047  tfrlem7  7648  omword  7819  isinf  8338  fsuppunbi  8461  axdc3lem2  9465  supsrlem  10124  expclzlem  13078  expgt0  13087  expge0  13090  expge1  13091  swrdnd2  13633  resqrex  14190  rplpwr  15478  4sqlem19  15869  gexcl3  18202  thlle  20243  decpmataa0  20775  neindisj  21123  ptcmplem5  22061  tsmsxplem1  22157  tsmsxplem2  22158  elovolmr  23444  itgsubst  24011  logeftb  24529  logbchbase  24708  legov  25679  unopbd  29183  nmcoplb  29198  nmcfnlb  29222  nmopcoi  29263  iocinif  29852  voliune  30601  signstfvneq0  30958  nosupbnd1lem5  32164  f1omptsnlem  33494  unccur  33705  matunitlindflem2  33719  stoweidlem15  40735  hoiqssbllem3  41344  vonioo  41402  vonicc  41405  gboge9  42162
  Copyright terms: Public domain W3C validator