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  3147  eloprabga  6097  ereldm  6733  mapen  7015  ordiso2  7213  subcan  8412  conjmulap  8887  ltrec  9041  divelunit  10210  fseq1m1p1  10303  fzm1  10308  qsqeqor  10884  fihashneq0  11028  hashfacen  11071  ccat0  11144  cvg1nlemcau  11510  lenegsq  11621  dvdsmod  12388  bitsmod  12482  bezoutlemle  12544  rpexp  12690  qnumdenbi  12729  eulerthlemh  12768  odzdvds  12783  pcelnn  12859  grpidpropdg  13422  sgrppropd  13461  mndpropd  13488  mhmpropd  13514  grppropd  13565  ghmnsgima  13820  cmnpropd  13847  qusecsub  13883  rngpropd  13933  ringpropd  14016  dvdsrpropdg  14126  resrhm2b  14228  lmodprop2d  14327  lsspropdg  14410  zndvds0  14629  bdxmet  15190  txmetcnp  15207  cnmet  15219  lgsne0  15732  lgsabs1  15733  gausslemma2dlem1a  15752  lgsquadlem2  15772  usgredg2v  16037  wlkeq  16095