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  3161  eloprabga  6140  ereldm  6812  mapen  7099  ordiso2  7326  subcan  8528  conjmulap  9003  ltrec  9157  divelunit  10335  fseq1m1p1  10429  fzm1  10434  qsqeqor  11012  fihashneq0  11157  hashfacen  11208  ccat0  11284  cvg1nlemcau  11669  lenegsq  11780  dvdsmod  12548  bitsmod  12642  bezoutlemle  12704  rpexp  12850  qnumdenbi  12889  eulerthlemh  12928  odzdvds  12943  pcelnn  13019  grpidpropdg  13587  sgrppropd  13626  mndpropd  13653  mhmpropd  13679  grppropd  13730  ghmnsgima  13985  cmnpropd  14012  qusecsub  14048  rngpropd  14099  ringpropd  14182  dvdsrpropdg  14292  resrhm2b  14394  lmodprop2d  14496  lsspropdg  14579  zndvds0  14798  bdxmet  15366  txmetcnp  15383  cnmet  15395  lgsne0  15911  lgsabs1  15912  gausslemma2dlem1a  15931  lgsquadlem2  15951  usgredg2v  16219  wlkeq  16349  eupth2lem3lem3fi  16465  eupth2lem3lem6fi  16466