MPE Home 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