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

Theorem 3bitr3rd 276
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr3d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr3d.2  |-  ( ph  ->  ( ps  <->  th )
)
3bitr3d.3  |-  ( ph  ->  ( ch  <->  ta )
)
Assertion
Ref Expression
3bitr3rd  |-  ( ph  ->  ( ta  <->  th )
)

Proof of Theorem 3bitr3rd
StepHypRef Expression
1 3bitr3d.3 . 2  |-  ( ph  ->  ( ch  <->  ta )
)
2 3bitr3d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
3 3bitr3d.2 . . 3  |-  ( ph  ->  ( ps  <->  th )
)
42, 3bitr3d 247 . 2  |-  ( ph  ->  ( ch  <->  th )
)
51, 4bitr3d 247 1  |-  ( ph  ->  ( ta  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  wdomtr  7503  ltaddsub  9462  leaddsub  9464  eqneg  9694  sqreulem  12122  nmzsubg  14940  dfod2  15159  odf1o2  15166  cyggenod  15453  lvecvscan  16142  znidomb  16801  iccpnfcnv  18926  dvcvx  19861  cxple2  20545  wilthlem1  20808  lgslem1  21037  hvmulcan  22531  unopf1o  23376  ballotlemrv  24734  subfacp1lem3  24825  subfacp1lem5  24827  colinearalglem2  25754  axeuclidlem  25809  axcontlem7  25817  areacirclem2  26185  areacirc  26191  rmxdiophlem  26980  f1omvdconj  27261  cdleme50eq  31027  hdmapeq0  32334  hdmap11  32338
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 178
  Copyright terms: Public domain W3C validator