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  3151  eloprabga  6118  ereldm  6790  mapen  7075  ordiso2  7277  subcan  8476  conjmulap  8951  ltrec  9105  divelunit  10281  fseq1m1p1  10375  fzm1  10380  qsqeqor  10958  fihashneq0  11102  hashfacen  11146  ccat0  11222  cvg1nlemcau  11607  lenegsq  11718  dvdsmod  12486  bitsmod  12580  bezoutlemle  12642  rpexp  12788  qnumdenbi  12827  eulerthlemh  12866  odzdvds  12881  pcelnn  12957  grpidpropdg  13520  sgrppropd  13559  mndpropd  13586  mhmpropd  13612  grppropd  13663  ghmnsgima  13918  cmnpropd  13945  qusecsub  13981  rngpropd  14032  ringpropd  14115  dvdsrpropdg  14225  resrhm2b  14327  lmodprop2d  14427  lsspropdg  14510  zndvds0  14729  bdxmet  15295  txmetcnp  15312  cnmet  15324  lgsne0  15840  lgsabs1  15841  gausslemma2dlem1a  15860  lgsquadlem2  15880  usgredg2v  16148  wlkeq  16278  eupth2lem3lem3fi  16394  eupth2lem3lem6fi  16395