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  7305  ltaddsub  9264  leaddsub  9266  eqneg  9496  sqreulem  11859  nmzsubg  14674  dfod2  14893  odf1o2  14900  cyggenod  15187  lvecvscan  15880  znidomb  16531  iccpnfcnv  18458  dvcvx  19383  cxple2  20060  wilthlem1  20322  lgslem1  20551  hvmulcan  21667  unopf1o  22512  subfacp1lem3  23728  subfacp1lem5  23730  colinearalglem2  24607  axeuclidlem  24662  axcontlem7  24670  areacirclem2  25028  areacirc  25034  rmxdiophlem  27211  f1omvdconj  27492  cdleme50eq  31352  hdmapeq0  32659  hdmap11  32663
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