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

Theorem syl2anbr 592
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 577 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2br 588 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386
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 199  df-an 387
This theorem is referenced by:  sylancbr  594  reusv2  5105  tz6.12  6460  r1ord3  8929  brdom7disj  9675  brdom6disj  9676  alephadd  9721  ltresr  10284  divmuldiv  11058  fnn0ind  11811  rexanuz  14469  nprmi  15781  lsmvalx  18412  cncfval  23068  angval  24948  amgmlem  25136  sspval  28129  sshjval  28760  sshjval3  28764  hosmval  29145  hodmval  29147  hfsmval  29148  broutsideof3  32767  mptsnunlem  33730  relowlpssretop  33756  line2ylem  43317
  Copyright terms: Public domain W3C validator