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  7376  subcan  8583  conjmulap  9062  ltrec  9216  divelunit  10415  fseq1m1p1  10513  fzm1  10518  qsqeqor  11102  fihashneq0  11249  hashfacen  11300  hashf1  11303  ccat0  11380  cvg1nlemcau  11766  lenegsq  11878  dvdsmod  12648  bitsmod  12742  bezoutlemle  12804  rpexp  12951  qnumdenbi  12991  eulerthlemh  13032  odzdvds  13047  pcelnn  13123  ballotfilemfc0  13284  ballotfilemfcc  13285  grpidpropdg  13747  sgrppropd  13781  mndpropd  13806  mhmpropd  13826  grppropd  13875  ghmnsgima  14124  cmnpropd  14182  qusecsub  14219  rngpropd  14338  ringpropd  14427  dvdsrpropdg  14538  resrhm2b  14641  opprdrng  14704  lmodprop2d  14769  lsspropdg  14852  zndvds0  15069  assapropd  15098  bdxmet  15693  txmetcnp  15710  cnmet  15722  birthdaylem3  16188  bposlem7  16278  lgsne0  16323  lgsabs1  16324  gausslemma2dlem1a  16343  lgsquadlem2  16363  usgredg2v  16631  wlkeq  16761  eupth2lem3lem3fi  16877  eupth2lem3lem6fi  16878