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

Theorem syl2anbr 598
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 581 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2br 594 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  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 206  df-an 396
This theorem is referenced by:  sylancbr  600  reusv2  5391  rexopabb  5518  tz6.12  6906  r1ord3  9772  brdom7disj  10521  brdom6disj  10522  alephadd  10567  ltresr  11130  divmuldiv  11910  fnn0ind  12657  rexanuz  15288  nprmi  16622  lsmvalx  19544  cncfval  24718  angval  26637  amgmlem  26826  sspval  30400  sshjval  31027  sshjval3  31031  hosmval  31412  hodmval  31414  hfsmval  31415  opreu2reuALT  32141  broutsideof3  35559  mptsnunlem  36675  relowlpssretop  36701  line2ylem  47591
  Copyright terms: Public domain W3C validator