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

Theorem syl2anbr 602
Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
Hypotheses
Ref Expression
syl2anbr.1 (𝜓𝜑)
syl2anbr.2 (𝜒𝜏)
syl2anbr.3 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
syl2anbr ((𝜑𝜏) → 𝜃)

Proof of Theorem syl2anbr
StepHypRef Expression
1 syl2anbr.2 . 2 (𝜒𝜏)
2 syl2anbr.1 . . 3 (𝜓𝜑)
3 syl2anbr.3 . . 3 ((𝜓𝜒) → 𝜃)
42, 3sylanbr 585 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2br 598 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:  sylancbr  604  reusv2  5305  rexopabb  5418  tz6.12  6749  r1ord3  9411  brdom7disj  10158  brdom6disj  10159  alephadd  10204  ltresr  10767  divmuldiv  11545  fnn0ind  12289  rexanuz  14922  nprmi  16259  lsmvalx  19041  cncfval  23798  angval  25697  amgmlem  25885  sspval  28817  sshjval  29444  sshjval3  29448  hosmval  29829  hodmval  29831  hfsmval  29832  opreu2reuALT  30557  broutsideof3  34178  mptsnunlem  35259  relowlpssretop  35285  line2ylem  45785
  Copyright terms: Public domain W3C validator