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  3150  eloprabga  6108  ereldm  6747  mapen  7032  ordiso2  7234  subcan  8434  conjmulap  8909  ltrec  9063  divelunit  10237  fseq1m1p1  10330  fzm1  10335  qsqeqor  10913  fihashneq0  11057  hashfacen  11101  ccat0  11177  cvg1nlemcau  11562  lenegsq  11673  dvdsmod  12441  bitsmod  12535  bezoutlemle  12597  rpexp  12743  qnumdenbi  12782  eulerthlemh  12821  odzdvds  12836  pcelnn  12912  grpidpropdg  13475  sgrppropd  13514  mndpropd  13541  mhmpropd  13567  grppropd  13618  ghmnsgima  13873  cmnpropd  13900  qusecsub  13936  rngpropd  13987  ringpropd  14070  dvdsrpropdg  14180  resrhm2b  14282  lmodprop2d  14381  lsspropdg  14464  zndvds0  14683  bdxmet  15244  txmetcnp  15261  cnmet  15273  lgsne0  15786  lgsabs1  15787  gausslemma2dlem1a  15806  lgsquadlem2  15826  usgredg2v  16094  wlkeq  16224  eupth2lem3lem3fi  16340  eupth2lem3lem6fi  16341