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  7990  ltaddsub  10015  leaddsub  10017  eqneg  10253  sqreulem  13141  nmzsubg  16030  f1omvdconj  16260  dfod2  16375  odf1o2  16382  cyggenod  16671  lvecvscan  17533  znidomb  18360  mdetunilem9  18882  iccpnfcnv  21172  dvcvx  22149  cxple2  22799  wilthlem1  23063  lgslem1  23292  colinearalglem2  23879  axeuclidlem  23934  axcontlem7  23942  hvmulcan  25515  unopf1o  26361  ballotlemrv  27948  subfacp1lem3  28116  subfacp1lem5  28118  dvtanlem  29492  areacirclem1  29535  areacirc  29540  rmxdiophlem  30414  cdleme50eq  35212  hdmapeq0  36519  hdmap11  36523
  Copyright terms: Public domain W3C validator