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

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

Proof of Theorem 3bitr2d
StepHypRef Expression
1 3bitr2d.1 . . 3
2 3bitr2d.2 . . 3
31, 2bitr4d 256 . 2
4 3bitr2d.3 . 2
53, 4bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  ceqsralt  3133  raltpd  4153  opiota  6859  adderpqlem  9353  mulerpqlem  9354  lesub2  10072  rec11  10267  avglt1  10801  ixxun  11574  hashdom  12447  hashf1lem1  12504  swrdspsleq  12673  repsdf2  12750  2shfti  12913  mulre  12954  rlim  13318  rlim2  13319  nn0seqcvgd  14199  prmreclem6  14439  pwsleval  14890  issubc  15204  ismgmid  15891  grpsubeq0  16124  grpsubadd  16126  gastacos  16348  orbsta  16351  lsslss  17607  coe1mul2lem1  18308  prmirredlem  18523  prmirredlemOLD  18526  zndvds  18588  zntoslem  18595  cygznlem1  18605  islindf2  18849  restcld  19673  leordtvallem1  19711  leordtvallem2  19712  ist1-2  19848  xkoccn  20120  qtopcld  20214  ordthmeolem  20302  qustgpopn  20618  isxmet2d  20830  prdsxmetlem  20871  xblss2  20905  imasf1oxms  20992  neibl  21004  xrtgioo  21311  xrsxmet  21314  minveclem4  21847  minveclem6  21849  minveclem7  21850  mbfmulc2lem  22054  mbfmax  22056  mbfi1fseqlem4  22125  itg2gt0  22167  itg2cnlem2  22169  iblpos  22199  angrteqvd  23138  affineequiv  23157  affineequiv2  23158  dcubic  23177  rlimcnp  23295  rlimcnp2  23296  efexple  23556  bposlem7  23565  lgsabs1  23609  lgsquadlem1  23629  m1lgs  23637  colinearalg  24213  axcontlem2  24268  nb3grapr  24453  el2wlksotot  24882  rusgranumwlkl1  24947  numclwlk1lem2f1  25094  minvecolem4  25796  minvecolem6  25798  minvecolem7  25799  hvmulcan2  25990  xppreima  27487  pstmxmet  27876  xrge0iifcnv  27915  ballotlemsima  28454  itg2addnclem  30066  itg2addnclem2  30067  iblabsnclem  30078  areacirclem2  30108  areacirclem4  30110  dvdsabsmod0  30928  radcnvrat  31195  cvlcvrp  35065
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