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  3068  eloprabga  5929  ereldm  6544  mapen  6812  ordiso2  7000  subcan  8153  conjmulap  8625  ltrec  8778  divelunit  9938  fseq1m1p1  10030  fzm1  10035  qsqeqor  10565  fihashneq0  10708  hashfacen  10749  cvg1nlemcau  10926  lenegsq  11037  dvdsmod  11800  bezoutlemle  11941  rpexp  12085  qnumdenbi  12124  eulerthlemh  12163  odzdvds  12177  pcelnn  12252  grpidpropdg  12605  bdxmet  13141  txmetcnp  13158  cnmet  13170  lgsne0  13579  lgsabs1  13580