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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  csbcomg  3170  eloprabga  6175  ereldm  6852  mapen  7146  ordiso2  7375  subcan  8582  conjmulap  9061  ltrec  9215  divelunit  10414  fseq1m1p1  10512  fzm1  10517  qsqeqor  11100  fihashneq0  11247  hashfacen  11298  hashf1  11301  ccat0  11378  cvg1nlemcau  11764  lenegsq  11876  dvdsmod  12645  bitsmod  12739  bezoutlemle  12801  rpexp  12948  qnumdenbi  12988  eulerthlemh  13029  odzdvds  13044  pcelnn  13120  ballotfilemfc0  13281  ballotfilemfcc  13282  grpidpropdg  13743  sgrppropd  13777  mndpropd  13802  mhmpropd  13822  grppropd  13871  ghmnsgima  14120  cmnpropd  14147  qusecsub  14184  rngpropd  14303  ringpropd  14392  dvdsrpropdg  14503  resrhm2b  14606  opprdrng  14669  lmodprop2d  14734  lsspropdg  14817  zndvds0  15034  assapropd  15063  bdxmet  15651  txmetcnp  15668  cnmet  15680  birthdaylem3  16146  lgsne0  16255  lgsabs1  16256  gausslemma2dlem1a  16275  lgsquadlem2  16295  usgredg2v  16563  wlkeq  16693  eupth2lem3lem3fi  16809  eupth2lem3lem6fi  16810