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

Theorem 3bitr3rd 275
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 246 . 2  |-  ( ph  ->  ( ch  <->  th )
)
51, 4bitr3d 246 1  |-  ( ph  ->  ( ta  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  wdomtr  7289  ltaddsub  9248  leaddsub  9250  eqneg  9480  sqreulem  11843  nmzsubg  14658  dfod2  14877  odf1o2  14884  cyggenod  15171  lvecvscan  15864  znidomb  16515  iccpnfcnv  18442  dvcvx  19367  cxple2  20044  wilthlem1  20306  lgslem1  20535  hvmulcan  21651  unopf1o  22496  subfacp1lem3  23713  subfacp1lem5  23715  colinearalglem2  24535  axeuclidlem  24590  axcontlem7  24598  areacirclem2  24925  areacirc  24931  rmxdiophlem  27108  f1omvdconj  27389  cdleme50eq  30730  hdmapeq0  32037  hdmap11  32041
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 177
  Copyright terms: Public domain W3C validator