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  7477  ltaddsub  9435  leaddsub  9437  eqneg  9667  sqreulem  12091  nmzsubg  14909  dfod2  15128  odf1o2  15135  cyggenod  15422  lvecvscan  16111  znidomb  16766  iccpnfcnv  18841  dvcvx  19772  cxple2  20456  wilthlem1  20719  lgslem1  20948  hvmulcan  22423  unopf1o  23268  ballotlemrv  24557  subfacp1lem3  24648  subfacp1lem5  24650  colinearalglem2  25561  axeuclidlem  25616  axcontlem7  25624  areacirclem2  25983  areacirc  25989  rmxdiophlem  26778  f1omvdconj  27059  cdleme50eq  30656  hdmapeq0  31963  hdmap11  31967
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