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

Theorem syl2anbr 588
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 573 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2br 584 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  sylancbr  590  reusv2  5085  tz6.12  6441  r1ord3  8902  brdom7disj  9648  brdom6disj  9649  alephadd  9694  ltresr  10256  divmuldiv  11020  fnn0ind  11762  rexanuz  14328  nprmi  15640  lsmvalx  18275  cncfval  22925  angval  24768  amgmlem  24953  sspval  27929  sshjval  28560  sshjval3  28564  hosmval  28945  hodmval  28947  hfsmval  28948  broutsideof3  32576  mptsnunlem  33521  relowlpssretop  33547
  Copyright terms: Public domain W3C validator