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

Theorem syl2anbr 480
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 473 . 2
51, 4sylan2br 476 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  sylancbr  666  pm2.61iineOLD  2780  reusv2  4658  tz6.12  5888  r1ord3  8221  brdom7disj  8930  brdom6disj  8931  alephadd  8973  ltresr  9538  divmuldiv  10269  fnn0ind  10988  rexanuz  13178  nprmi  14232  lsmvalx  16659  cncfval  21392  angval  23133  amgmlem  23319  sspval  25636  sshjval  26268  sshjval3  26272  hosmval  26654  hodmval  26656  hfsmval  26657  broutsideof3  29776
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 185  df-an 371
  Copyright terms: Public domain W3C validator