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

Theorem syl2anbr 599
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 582 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2br 595 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395
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 207  df-an 396
This theorem is referenced by:  sylancbr  601  reusv2  5402  rexopabb  5532  tz6.12  6930  r1ord3  9823  brdom7disj  10572  brdom6disj  10573  alephadd  10618  ltresr  11181  divmuldiv  11968  fnn0ind  12719  rexanuz  15385  nprmi  16727  lsmvalx  19658  cncfval  24915  angval  26845  amgmlem  27034  sspval  30743  sshjval  31370  sshjval3  31374  hosmval  31755  hodmval  31757  hfsmval  31758  opreu2reuALT  32497  broutsideof3  36128  mptsnunlem  37340  relowlpssretop  37366  line2ylem  48677
  Copyright terms: Public domain W3C validator