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  6178  ereldm  6857  mapen  7152  ordiso2  7381  subcan  8588  conjmulap  9067  ltrec  9221  divelunit  10420  fseq1m1p1  10518  fzm1  10523  qsqeqor  11107  fihashneq0  11254  hashfacen  11305  hashf1  11308  ccat0  11385  cvg1nlemcau  11771  lenegsq  11883  dvdsmod  12653  bitsmod  12747  bezoutlemle  12809  rpexp  12956  qnumdenbi  12996  eulerthlemh  13037  odzdvds  13052  pcelnn  13128  ballotfilemfc0  13289  ballotfilemfcc  13290  grpidpropdg  13752  sgrppropd  13786  mndpropd  13811  mhmpropd  13831  grppropd  13880  ghmnsgima  14129  cmnpropd  14187  qusecsub  14224  rngpropd  14360  ringpropd  14449  dvdsrpropdg  14562  resrhm2b  14665  opprdrng  14728  lmodprop2d  14793  lsspropdg  14876  zndvds0  15093  assapropd  15122  bdxmet  15744  txmetcnp  15761  cnmet  15773  birthdaylem3  16244  bposlem7  16334  lgsne0  16379  lgsabs1  16380  gausslemma2dlem1a  16399  lgsquadlem2  16419  usgredg2v  16687  wlkeq  16817  eupth2lem3lem3fi  16933  eupth2lem3lem6fi  16934