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

Theorem syl2anbr 496
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 489 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2br 492 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 385
This theorem is referenced by:  sylancbr  701  reusv2  4904  tz6.12  6249  r1ord3  8683  brdom7disj  9391  brdom6disj  9392  alephadd  9437  ltresr  9999  divmuldiv  10763  fnn0ind  11514  rexanuz  14129  nprmi  15449  lsmvalx  18100  cncfval  22738  angval  24576  amgmlem  24761  sspval  27706  sshjval  28337  sshjval3  28341  hosmval  28722  hodmval  28724  hfsmval  28725  broutsideof3  32358  mptsnunlem  33315  relowlpssretop  33342
  Copyright terms: Public domain W3C validator