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

Theorem 3bitr3rd 277
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 248 . 2  |-  ( ph  ->  ( ch  <->  th )
)
51, 4bitr3d 248 1  |-  ( ph  ->  ( ta  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  wdomtr  7546  ltaddsub  9507  leaddsub  9509  eqneg  9739  sqreulem  12168  nmzsubg  14986  dfod2  15205  odf1o2  15212  cyggenod  15499  lvecvscan  16188  znidomb  16847  iccpnfcnv  18974  dvcvx  19909  cxple2  20593  wilthlem1  20856  lgslem1  21085  hvmulcan  22579  unopf1o  23424  ballotlemrv  24782  subfacp1lem3  24873  subfacp1lem5  24875  colinearalglem2  25851  axeuclidlem  25906  axcontlem7  25914  dvtanlem  26268  areacirclem1  26306  areacirc  26311  rmxdiophlem  27100  f1omvdconj  27380  cdleme50eq  31412  hdmapeq0  32719  hdmap11  32723
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 179
  Copyright terms: Public domain W3C validator