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  3120  eloprabga  6045  ereldm  6678  mapen  6958  ordiso2  7152  subcan  8347  conjmulap  8822  ltrec  8976  divelunit  10144  fseq1m1p1  10237  fzm1  10242  qsqeqor  10817  fihashneq0  10961  hashfacen  11003  ccat0  11075  cvg1nlemcau  11370  lenegsq  11481  dvdsmod  12248  bitsmod  12342  bezoutlemle  12404  rpexp  12550  qnumdenbi  12589  eulerthlemh  12628  odzdvds  12643  pcelnn  12719  grpidpropdg  13281  sgrppropd  13320  mndpropd  13347  mhmpropd  13373  grppropd  13424  ghmnsgima  13679  cmnpropd  13706  qusecsub  13742  rngpropd  13792  ringpropd  13875  dvdsrpropdg  13984  resrhm2b  14086  lmodprop2d  14185  lsspropdg  14268  zndvds0  14487  bdxmet  15048  txmetcnp  15065  cnmet  15077  lgsne0  15590  lgsabs1  15591  gausslemma2dlem1a  15610  lgsquadlem2  15630