Theorem 3bitr3rd 299

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

Step	Hyp	Ref	Expression
1		3bitr3d.3	. 2 |- ( ph -> ( ch <-> ta ) )
2		3bitr3d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3		3bitr3d.2	. . 3 |- ( ph -> ( ps <-> th ) )
4	2, 3	bitr3d 270	. 2 |- ( ph -> ( ch <-> th ) )
5	1, 4	bitr3d 270	1 |- ( ph -> ( ta <-> th ) )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  wdomtr  8480  ltaddsub  10502  leaddsub  10504  eqneg  10745  sqreulem  14099  brcic  16458  nmzsubg  17635  f1omvdconj  17866  dfod2  17981  odf1o2  17988  cyggenod  18286  lvecvscan  19111  znidomb  19910  mdetunilem9  20426  iccpnfcnv  22743  dvcvx  23783  cxple2  24443  wilthlem1  24794  lgslem1  25022  colinearalglem2  25787  axeuclidlem  25842  axcontlem7  25850  fusgrfisstep  26221  hvmulcan  27929  unopf1o  28775  ballotlemrv  30581  subfacp1lem3  31164  subfacp1lem5  31166  wl-sbcom2d  33344  poimirlem26  33435  areacirclem1  33500  areacirc  33505  cdleme50eq  35829  hdmapeq0  37136  hdmap11  37140  rmxdiophlem  37582  nnsum3primesle9  41682  0ringdif  41870