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  3104  eloprabga  6006  ereldm  6634  mapen  6904  ordiso2  7096  subcan  8276  conjmulap  8750  ltrec  8904  divelunit  10071  fseq1m1p1  10164  fzm1  10169  qsqeqor  10724  fihashneq0  10868  hashfacen  10910  cvg1nlemcau  11131  lenegsq  11242  dvdsmod  12007  bezoutlemle  12148  rpexp  12294  qnumdenbi  12333  eulerthlemh  12372  odzdvds  12386  pcelnn  12462  grpidpropdg  12960  sgrppropd  12999  mndpropd  13024  mhmpropd  13041  grppropd  13092  ghmnsgima  13341  cmnpropd  13368  qusecsub  13404  rngpropd  13454  ringpropd  13537  dvdsrpropdg  13646  resrhm2b  13748  lmodprop2d  13847  lsspropdg  13930  zndvds0  14149  bdxmet  14680  txmetcnp  14697  cnmet  14709  lgsne0  15195  lgsabs1  15196  gausslemma2dlem1a  15215  lgsquadlem2  15235