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

Theorem syl2anbr 497
 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 490 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2br 493 1 ((𝜑𝜏) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384 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 386 This theorem is referenced by:  sylancbr  699  reusv2  4844  tz6.12  6178  r1ord3  8605  brdom7disj  9313  brdom6disj  9314  alephadd  9359  ltresr  9921  divmuldiv  10685  fnn0ind  11436  rexanuz  14035  nprmi  15345  lsmvalx  17994  cncfval  22631  angval  24465  amgmlem  24650  sspval  27466  sshjval  28097  sshjval3  28101  hosmval  28482  hodmval  28484  hfsmval  28485  broutsideof3  31928  mptsnunlem  32856  relowlpssretop  32883
 Copyright terms: Public domain W3C validator