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

Theorem 3bitrrd 273
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitrd.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitrd.2  |-  ( ph  ->  ( ch  <->  th )
)
3bitrd.3  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
3bitrrd  |-  ( ph  ->  ( ta  <->  ps )
)

Proof of Theorem 3bitrrd
StepHypRef Expression
1 3bitrd.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
2 3bitrd.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
3 3bitrd.2 . . 3  |-  ( ph  ->  ( ch  <->  th )
)
42, 3bitr2d 247 . 2  |-  ( ph  ->  ( th  <->  ps )
)
51, 4bitr3d 248 1  |-  ( ph  ->  ( ta  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  fnwelem  6464  compssiso  8259  cjreb  11933  cnpart  12050  bitsuz  12991  acsfn  13889  ghmeqker  15037  odmulg  15197  psrbaglefi  16442  cnrest2  17355  hausdiag  17682  prdsbl  18526  mcubic  20692  cusgra3v  21478  areacirclem4  26309  lmclim2  26478  expdiophlem1  27106  cmtbr2N  30125
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 179
  Copyright terms: Public domain W3C validator