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

Theorem 3bitrrd 271
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 245 . 2  |-  ( ph  ->  ( th  <->  ps )
)
51, 4bitr3d 246 1  |-  ( ph  ->  ( ta  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  fnwelem  6246  compssiso  8016  cjreb  11624  cnpart  11741  bitsuz  12681  acsfn  13577  ghmeqker  14725  odmulg  14885  psrbaglefi  16134  cnrest2  17030  hausdiag  17355  prdsbl  18053  mcubic  20159  areacirclem5  25032  lmclim2  26577  expdiophlem1  27217  cusgra3v  28299  cmtbr2N  30065
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator