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  6107  ereldm  6746  mapen  7031  ordiso2  7233  subcan  8433  conjmulap  8908  ltrec  9062  divelunit  10236  fseq1m1p1  10329  fzm1  10334  qsqeqor  10911  fihashneq0  11055  hashfacen  11099  ccat0  11172  cvg1nlemcau  11544  lenegsq  11655  dvdsmod  12422  bitsmod  12516  bezoutlemle  12578  rpexp  12724  qnumdenbi  12763  eulerthlemh  12802  odzdvds  12817  pcelnn  12893  grpidpropdg  13456  sgrppropd  13495  mndpropd  13522  mhmpropd  13548  grppropd  13599  ghmnsgima  13854  cmnpropd  13881  qusecsub  13917  rngpropd  13967  ringpropd  14050  dvdsrpropdg  14160  resrhm2b  14262  lmodprop2d  14361  lsspropdg  14444  zndvds0  14663  bdxmet  15224  txmetcnp  15241  cnmet  15253  lgsne0  15766  lgsabs1  15767  gausslemma2dlem1a  15786  lgsquadlem2  15806  usgredg2v  16074  wlkeq  16204