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  3147  eloprabga  6090  ereldm  6723  mapen  7003  ordiso2  7198  subcan  8397  conjmulap  8872  ltrec  9026  divelunit  10194  fseq1m1p1  10287  fzm1  10292  qsqeqor  10867  fihashneq0  11011  hashfacen  11053  ccat0  11126  cvg1nlemcau  11490  lenegsq  11601  dvdsmod  12368  bitsmod  12462  bezoutlemle  12524  rpexp  12670  qnumdenbi  12709  eulerthlemh  12748  odzdvds  12763  pcelnn  12839  grpidpropdg  13402  sgrppropd  13441  mndpropd  13468  mhmpropd  13494  grppropd  13545  ghmnsgima  13800  cmnpropd  13827  qusecsub  13863  rngpropd  13913  ringpropd  13996  dvdsrpropdg  14105  resrhm2b  14207  lmodprop2d  14306  lsspropdg  14389  zndvds0  14608  bdxmet  15169  txmetcnp  15186  cnmet  15198  lgsne0  15711  lgsabs1  15712  gausslemma2dlem1a  15731  lgsquadlem2  15751  usgredg2v  16016