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  7993  ltaddsub  10022  leaddsub  10024  eqneg  10260  sqreulem  13274  brcic  15286  nmzsubg  16441  f1omvdconj  16670  dfod2  16785  odf1o2  16792  cyggenod  17086  lvecvscan  17952  znidomb  18773  mdetunilem9  19289  iccpnfcnv  21610  dvcvx  22587  cxple2  23246  wilthlem1  23540  lgslem1  23769  colinearalglem2  24412  axeuclidlem  24467  axcontlem7  24475  hvmulcan  26187  unopf1o  27033  ballotlemrv  28722  subfacp1lem3  28890  subfacp1lem5  28892  wl-sbcom2d  30251  dvtanlem  30304  areacirclem1  30347  areacirc  30352  rmxdiophlem  31196  0ringdif  32930  cdleme50eq  36664  hdmapeq0  37971  hdmap11  37975
  Copyright terms: Public domain W3C validator