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  3148  eloprabga  6103  ereldm  6742  mapen  7027  ordiso2  7225  subcan  8424  conjmulap  8899  ltrec  9053  divelunit  10227  fseq1m1p1  10320  fzm1  10325  qsqeqor  10902  fihashneq0  11046  hashfacen  11090  ccat0  11163  cvg1nlemcau  11535  lenegsq  11646  dvdsmod  12413  bitsmod  12507  bezoutlemle  12569  rpexp  12715  qnumdenbi  12754  eulerthlemh  12793  odzdvds  12808  pcelnn  12884  grpidpropdg  13447  sgrppropd  13486  mndpropd  13513  mhmpropd  13539  grppropd  13590  ghmnsgima  13845  cmnpropd  13872  qusecsub  13908  rngpropd  13958  ringpropd  14041  dvdsrpropdg  14151  resrhm2b  14253  lmodprop2d  14352  lsspropdg  14435  zndvds0  14654  bdxmet  15215  txmetcnp  15232  cnmet  15244  lgsne0  15757  lgsabs1  15758  gausslemma2dlem1a  15777  lgsquadlem2  15797  usgredg2v  16063  wlkeq  16151