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 584 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2br 596 1 ((𝜑𝜏) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  sylancbr  602  reusv2  5294  rexopabb  5406  tz6.12  6686  r1ord3  9203  brdom7disj  9945  brdom6disj  9946  alephadd  9991  ltresr  10554  divmuldiv  11332  fnn0ind  12073  rexanuz  14697  nprmi  16025  lsmvalx  18756  cncfval  23488  angval  25371  amgmlem  25559  sspval  28492  sshjval  29119  sshjval3  29123  hosmval  29504  hodmval  29506  hfsmval  29507  opreu2reuALT  30232  broutsideof3  33575  mptsnunlem  34601  relowlpssretop  34627  line2ylem  44718
 Copyright terms: Public domain W3C validator