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  6463  compssiso  8256  cjreb  11930  cnpart  12047  bitsuz  12988  acsfn  13886  ghmeqker  15034  odmulg  15194  psrbaglefi  16439  cnrest2  17352  hausdiag  17679  prdsbl  18523  mcubic  20689  cusgra3v  21475  areacirclem4  26297  lmclim2  26466  expdiophlem1  27094  cmtbr2N  30053
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 179
  Copyright terms: Public domain W3C validator