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

Theorem 3bitr3rd 284
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 255 . 2  |-  ( ph  ->  ( ch  <->  th )
)
51, 4bitr3d 255 1  |-  ( ph  ->  ( ta  <->  th )
)
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:  wdomtr  7782  ltaddsub  9805  leaddsub  9807  eqneg  10043  sqreulem  12839  nmzsubg  15713  f1omvdconj  15943  dfod2  16056  odf1o2  16063  cyggenod  16352  lvecvscan  17169  znidomb  17969  mdetunilem9  18401  iccpnfcnv  20491  dvcvx  21467  cxple2  22117  wilthlem1  22381  lgslem1  22610  colinearalglem2  23104  axeuclidlem  23159  axcontlem7  23167  hvmulcan  24425  unopf1o  25271  ballotlemrv  26854  subfacp1lem3  27022  subfacp1lem5  27024  dvtanlem  28394  areacirclem1  28437  areacirc  28442  rmxdiophlem  29317  cdleme50eq  34025  hdmapeq0  35332  hdmap11  35336
  Copyright terms: Public domain W3C validator