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  6178  ereldm  6856  mapen  7150  ordiso2  7381  subcan  8588  conjmulap  9067  ltrec  9221  divelunit  10421  fseq1m1p1  10519  fzm1  10524  qsqeqor  11108  fihashneq0  11255  hashfacen  11306  hashf1  11309  ccat0  11386  cvg1nlemcau  11772  lenegsq  11884  dvdsmod  12654  bitsmod  12748  bezoutlemle  12810  rpexp  12957  qnumdenbi  12997  eulerthlemh  13038  odzdvds  13053  pcelnn  13129  ballotfilemfc0  13290  ballotfilemfcc  13291  grpidpropdg  13753  sgrppropd  13787  mndpropd  13812  mhmpropd  13832  grppropd  13881  ghmnsgima  14130  cmnpropd  14188  qusecsub  14225  rngpropd  14361  ringpropd  14450  dvdsrpropdg  14563  resrhm2b  14666  opprdrng  14729  lmodprop2d  14794  lsspropdg  14877  zndvds0  15094  assapropd  15123  bdxmet  15727  txmetcnp  15744  cnmet  15756  birthdaylem3  16227  bposlem7  16317  lgsne0  16362  lgsabs1  16363  gausslemma2dlem1a  16382  lgsquadlem2  16402  usgredg2v  16670  wlkeq  16800  eupth2lem3lem3fi  16916  eupth2lem3lem6fi  16917