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  3151  eloprabga  6118  ereldm  6790  mapen  7075  ordiso2  7277  subcan  8477  conjmulap  8952  ltrec  9106  divelunit  10280  fseq1m1p1  10373  fzm1  10378  qsqeqor  10956  fihashneq0  11100  hashfacen  11144  ccat0  11220  cvg1nlemcau  11605  lenegsq  11716  dvdsmod  12484  bitsmod  12578  bezoutlemle  12640  rpexp  12786  qnumdenbi  12825  eulerthlemh  12864  odzdvds  12879  pcelnn  12955  grpidpropdg  13518  sgrppropd  13557  mndpropd  13584  mhmpropd  13610  grppropd  13661  ghmnsgima  13916  cmnpropd  13943  qusecsub  13979  rngpropd  14030  ringpropd  14113  dvdsrpropdg  14223  resrhm2b  14325  lmodprop2d  14424  lsspropdg  14507  zndvds0  14726  bdxmet  15292  txmetcnp  15309  cnmet  15321  lgsne0  15834  lgsabs1  15835  gausslemma2dlem1a  15854  lgsquadlem2  15874  usgredg2v  16142  wlkeq  16272  eupth2lem3lem3fi  16388  eupth2lem3lem6fi  16389