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

Theorem syl2anbr 600
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 583 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2br 596 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 398
This theorem is referenced by:  sylancbr  602  reusv2  5362  rexopabb  5489  tz6.12  6871  r1ord3  9726  brdom7disj  10475  brdom6disj  10476  alephadd  10521  ltresr  11084  divmuldiv  11863  fnn0ind  12610  rexanuz  15239  nprmi  16573  lsmvalx  19429  cncfval  24274  angval  26174  amgmlem  26362  sspval  29714  sshjval  30341  sshjval3  30345  hosmval  30726  hodmval  30728  hfsmval  30729  opreu2reuALT  31455  broutsideof3  34764  mptsnunlem  35859  relowlpssretop  35885  line2ylem  46927
  Copyright terms: Public domain W3C validator