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  3103  eloprabga  6005  ereldm  6632  mapen  6902  ordiso2  7094  subcan  8274  conjmulap  8748  ltrec  8902  divelunit  10068  fseq1m1p1  10161  fzm1  10166  qsqeqor  10721  fihashneq0  10865  hashfacen  10907  cvg1nlemcau  11128  lenegsq  11239  dvdsmod  12004  bezoutlemle  12145  rpexp  12291  qnumdenbi  12330  eulerthlemh  12369  odzdvds  12383  pcelnn  12459  grpidpropdg  12957  sgrppropd  12996  mndpropd  13021  mhmpropd  13038  grppropd  13089  ghmnsgima  13338  cmnpropd  13365  qusecsub  13401  rngpropd  13451  ringpropd  13534  dvdsrpropdg  13643  resrhm2b  13745  lmodprop2d  13844  lsspropdg  13927  zndvds0  14138  bdxmet  14669  txmetcnp  14686  cnmet  14698  lgsne0  15154  lgsabs1  15155  gausslemma2dlem1a  15174