Theorem 3bitr3d 217

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)

Hypotheses

Ref	Expression
3bitr3d.1	|- ( ph -> ( ps <-> ch ) )
3bitr3d.2	|- ( ph -> ( ps <-> th ) )
3bitr3d.3	|- ( ph -> ( ch <-> ta ) )

Assertion

Ref	Expression
3bitr3d	|- ( ph -> ( th <-> ta ) )

Proof of Theorem 3bitr3d

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  csbcomg  3020  eloprabga  5851  ereldm  6465  mapen  6733  ordiso2  6913  subcan  8010  conjmulap  8482  ltrec  8634  divelunit  9778  fseq1m1p1  9868  fzm1  9873  fihashneq0  10534  hashfacen  10572  cvg1nlemcau  10749  lenegsq  10860  dvdsmod  11549  bezoutlemle  11685  rpexp  11820  qnumdenbi  11859  bdxmet  12659  txmetcnp  12676  cnmet  12688