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  6686  mpt2curryd  6787  compssiso  8542  cjreb  12611  cnpart  12728  bitsuz  13669  acsfn  14596  ghmeqker  15772  odmulg  16056  psrbaglefi  17440  psrbaglefiOLD  17441  cnrest2  18889  hausdiag  19217  prdsbl  20065  mcubic  22241  cusgra3v  23371  areacirclem4  28485  lmclim2  28652  expdiophlem1  29368  cmtbr2N  32896
  Copyright terms: Public domain W3C validator