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  3164  eloprabga  6148  ereldm  6825  mapen  7112  ordiso2  7339  subcan  8544  conjmulap  9020  ltrec  9174  divelunit  10354  fseq1m1p1  10451  fzm1  10456  qsqeqor  11036  fihashneq0  11182  hashfacen  11233  ccat0  11309  cvg1nlemcau  11694  lenegsq  11805  dvdsmod  12573  bitsmod  12667  bezoutlemle  12729  rpexp  12875  qnumdenbi  12914  eulerthlemh  12953  odzdvds  12968  pcelnn  13044  ballotfilemfc0  13176  ballotfilemfcc  13177  grpidpropdg  13637  sgrppropd  13676  mndpropd  13701  mhmpropd  13721  grppropd  13772  ghmnsgima  14021  cmnpropd  14048  qusecsub  14084  rngpropd  14194  ringpropd  14281  dvdsrpropdg  14392  resrhm2b  14495  opprdrng  14558  lmodprop2d  14622  lsspropdg  14705  zndvds0  14924  bdxmet  15492  txmetcnp  15509  cnmet  15521  lgsne0  16037  lgsabs1  16038  gausslemma2dlem1a  16057  lgsquadlem2  16077  usgredg2v  16345  wlkeq  16475  eupth2lem3lem3fi  16591  eupth2lem3lem6fi  16592