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

Theorem syl2anbr 482
 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 475 . 2
51, 4sylan2br 478 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370 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 188  df-an 372 This theorem is referenced by:  sylancbr  670  pm2.61iineOLD  2743  reusv2  4630  tz6.12  5898  r1ord3  8261  brdom7disj  8966  brdom6disj  8967  alephadd  9009  ltresr  9571  divmuldiv  10314  fnn0ind  11041  rexanuz  13408  nprmi  14638  lsmvalx  17290  cncfval  21918  angval  23728  amgmlem  23913  sspval  26360  sshjval  27001  sshjval3  27005  hosmval  27386  hodmval  27388  hfsmval  27389  broutsideof3  30898  mptsnunlem  31704  relowlpssretop  31731
 Copyright terms: Public domain W3C validator