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  7376  ltaddsub  9335  leaddsub  9337  eqneg  9567  sqreulem  11933  nmzsubg  14751  dfod2  14970  odf1o2  14977  cyggenod  15264  lvecvscan  15957  znidomb  16615  iccpnfcnv  18540  dvcvx  19465  cxple2  20149  wilthlem1  20412  lgslem1  20641  hvmulcan  21759  unopf1o  22604  subfacp1lem3  24117  subfacp1lem5  24119  colinearalglem2  25094  axeuclidlem  25149  axcontlem7  25157  areacirclem2  25517  areacirc  25523  rmxdiophlem  26431  f1omvdconj  26712  cdleme50eq  30782  hdmapeq0  32089  hdmap11  32093
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