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

Theorem 3bitr2rd 282
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2d.1
3bitr2d.2
3bitr2d.3
Assertion
Ref Expression
3bitr2rd

Proof of Theorem 3bitr2rd
StepHypRef Expression
1 3bitr2d.1 . . 3
2 3bitr2d.2 . . 3
31, 2bitr4d 256 . 2
4 3bitr2d.3 . 2
53, 4bitr2d 254 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  fnsuppresOLD  6131  fnsuppres  6946  addsubeq4  9858  muleqadd  10218  mulle0b  10438  nn0lt10bOLD  10951  om2uzlti  12061  qnumdenbi  14277  dprdf11  17063  dprdf11OLD  17070  lvecvscan2  17758  mplvalOLD  18085  mdetunilem9  19122  elfilss  20377  itg2seq  22149  itg2cnlem2  22169  chpchtsum  23494  bposlem7  23565  lgsdilem  23597  lgsne0  23608  axcontlem7  24273  pjnorm2  26645  cdj3lem1  27353  zrhchr  27957  dochfln0  37204  mapdindp  37398
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
  Copyright terms: Public domain W3C validator