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

Theorem 3bitrrd 283
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 257 . 2  |-  ( ph  ->  ( th  <->  ps )
)
51, 4bitr3d 258 1  |-  ( ph  ->  ( ta  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  fnwelem  6922  mpt2curryd  7024  compssiso  8802  cjreb  13165  cnpart  13282  bitsuz  14422  acsfn  15516  ghmeqker  16860  odmulg  17145  psrbaglefi  18531  cnrest2  20233  hausdiag  20591  prdsbl  21437  mcubic  23638  cusgra3v  25037  areacirclem4  31739  lmclim2  31791  cmtbr2N  32528  expdiophlem1  35582
  Copyright terms: Public domain W3C validator