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  7893  ltaddsub  9916  leaddsub  9918  eqneg  10154  sqreulem  12951  nmzsubg  15826  f1omvdconj  16056  dfod2  16171  odf1o2  16178  cyggenod  16467  lvecvscan  17300  znidomb  18105  mdetunilem9  18544  iccpnfcnv  20634  dvcvx  21610  cxple2  22260  wilthlem1  22524  lgslem1  22753  colinearalglem2  23290  axeuclidlem  23345  axcontlem7  23353  hvmulcan  24611  unopf1o  25457  ballotlemrv  27038  subfacp1lem3  27206  subfacp1lem5  27208  dvtanlem  28581  areacirclem1  28624  areacirc  28629  rmxdiophlem  29504  cdleme50eq  34493  hdmapeq0  35800  hdmap11  35804
  Copyright terms: Public domain W3C validator