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

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

Proof of Theorem 3bitrrd
StepHypRef Expression
1 3bitrd.3 . 2
2 3bitrd.1 . . 3
3 3bitrd.2 . . 3
42, 3bitr2d 254 . 2
51, 4bitr3d 255 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184 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 This theorem is referenced by:  fnwelem  6898  mpt2curryd  6998  compssiso  8754  cjreb  12919  cnpart  13036  bitsuz  13983  acsfn  14914  ghmeqker  16098  odmulg  16384  psrbaglefi  17822  psrbaglefiOLD  17823  cnrest2  19581  hausdiag  19909  prdsbl  20757  mcubic  22934  cusgra3v  24168  areacirclem4  29715  lmclim2  29882  expdiophlem1  30595  eliooshift  31133  cmtbr2N  34068
 Copyright terms: Public domain W3C validator