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

Theorem 3bitr3rd 276
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 247 . 2  |-  ( ph  ->  ( ch  <->  th )
)
51, 4bitr3d 247 1  |-  ( ph  ->  ( ta  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  wdomtr  7533  ltaddsub  9492  leaddsub  9494  eqneg  9724  sqreulem  12153  nmzsubg  14971  dfod2  15190  odf1o2  15197  cyggenod  15484  lvecvscan  16173  znidomb  16832  iccpnfcnv  18959  dvcvx  19894  cxple2  20578  wilthlem1  20841  lgslem1  21070  hvmulcan  22564  unopf1o  23409  ballotlemrv  24767  subfacp1lem3  24858  subfacp1lem5  24860  colinearalglem2  25811  axeuclidlem  25866  axcontlem7  25874  areacirclem2  26245  areacirc  26251  rmxdiophlem  27040  f1omvdconj  27321  cdleme50eq  31239  hdmapeq0  32546  hdmap11  32550
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 178
  Copyright terms: Public domain W3C validator