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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  csbcomg  3170  eloprabga  6175  ereldm  6852  mapen  7146  ordiso2  7375  subcan  8581  conjmulap  9059  ltrec  9213  divelunit  10404  fseq1m1p1  10502  fzm1  10507  qsqeqor  11087  fihashneq0  11233  hashfacen  11284  hashf1  11287  ccat0  11364  cvg1nlemcau  11750  lenegsq  11861  dvdsmod  12629  bitsmod  12723  bezoutlemle  12785  rpexp  12931  qnumdenbi  12970  eulerthlemh  13009  odzdvds  13024  pcelnn  13100  ballotfilemfc0  13232  ballotfilemfcc  13233  grpidpropdg  13694  sgrppropd  13728  mndpropd  13753  mhmpropd  13773  grppropd  13822  ghmnsgima  14071  cmnpropd  14098  qusecsub  14135  rngpropd  14254  ringpropd  14343  dvdsrpropdg  14454  resrhm2b  14557  opprdrng  14620  lmodprop2d  14685  lsspropdg  14768  zndvds0  14985  assapropd  15014  bdxmet  15602  txmetcnp  15619  cnmet  15631  birthdaylem3  16089  lgsne0  16157  lgsabs1  16158  gausslemma2dlem1a  16177  lgsquadlem2  16197  usgredg2v  16465  wlkeq  16595  eupth2lem3lem3fi  16711  eupth2lem3lem6fi  16712