MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitrrd 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 is referenced by:  fnwelem  6915  mpt2curryd  7017  compssiso  8775  cjreb  12956  cnpart  13073  bitsuz  14124  acsfn  15056  ghmeqker  16293  odmulg  16578  psrbaglefi  18023  psrbaglefiOLD  18024  cnrest2  19787  hausdiag  20146  prdsbl  20994  mcubic  23178  cusgra3v  24464  areacirclem4  30110  lmclim2  30251  expdiophlem1  30963  cmtbr2N  34978
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