Theorem 3bitr3d 218

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 190	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3d.3	. 2 |- ( ph -> ( ch <-> ta ) )
5	3, 4	bitrd 188	1 |- ( ph -> ( th <-> ta ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  csbcomg  3080  eloprabga  5961  ereldm  6577  mapen  6845  ordiso2  7033  subcan  8210  conjmulap  8684  ltrec  8838  divelunit  10000  fseq1m1p1  10092  fzm1  10097  qsqeqor  10627  fihashneq0  10769  hashfacen  10811  cvg1nlemcau  10988  lenegsq  11099  dvdsmod  11862  bezoutlemle  12003  rpexp  12147  qnumdenbi  12186  eulerthlemh  12225  odzdvds  12239  pcelnn  12314  grpidpropdg  12747  mndpropd  12795  mhmpropd  12811  grppropd  12847  cmnpropd  13051  ringpropd  13170  dvdsrpropdg  13269  bdxmet  13894  txmetcnp  13911  cnmet  13923  lgsne0  14332  lgsabs1  14333