MPE Home 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  |-  ( 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 254 . 2  |-  ( ph  ->  ( th  <->  ps )
)
51, 4bitr3d 255 1  |-  ( ph  ->  ( ta  <->  ps )
)
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