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  601  funfv  6738  2mpo0  7384  tfrlem7  8009  omword  8186  isinf  8722  fsuppunbi  8845  axdc3lem2  9865  supsrlem  10525  expclzlem  13454  expgt0  13463  expge0  13466  expge1  13467  swrdnd2  14013  resqrex  14606  rplpwr  15901  4sqlem19  16293  gexcl3  18708  thlle  20834  decpmataa0  21369  neindisj  21718  ptcmplem5  22657  tsmsxplem1  22754  tsmsxplem2  22755  elovolmr  24076  itgsubst  24648  logeftb  25171  logbchbase  25353  legov  26375  unopbd  29794  nmcoplb  29809  nmcfnlb  29833  nmopcoi  29874  iocinif  30508  voliune  31513  signstfvneq0  31867  lfuhgr3  32391  nosupbnd1lem5  33237  f1omptsnlem  34665  unccur  34950  matunitlindflem2  34964  stoweidlem15  42520  hoiqssbllem3  43126  vonioo  43184  vonicc  43187  gboge9  44145
  Copyright terms: Public domain W3C validator