Theorem 3bitr3g 221

Description: More general version of 3bitr3i 209. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)

Hypotheses

Ref	Expression
3bitr3g.1	|- ( ph -> ( ps <-> ch ) )
3bitr3g.2	|- ( ps <-> th )
3bitr3g.3	|- ( ch <-> ta )

Assertion

Ref	Expression
3bitr3g	|- ( ph -> ( th <-> ta ) )

Proof of Theorem 3bitr3g

Step	Hyp	Ref	Expression
1		3bitr3g.2	. . 3 |- ( ps <-> th )
2		3bitr3g.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3	1, 2	bitr3id 193	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3g.3	. 2 |- ( ch <-> ta )
5	3, 4	bitrdi 195	1 |- ( ph -> ( th <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  con2bidc  865  sbal1yz  1988  sbal1  1989  dfsbcq2  2949  iindif2m  3927  opeqex  4221  rabxfrd  4441  eqbrrdv  4695  eqbrrdiv  4696  opelco2g  4766  opelcnvg  4778  ralrnmpt  5621  rexrnmpt  5622  fliftcnv  5757  eusvobj2  5822  f1od2  6194  ottposg  6214  ercnv  6513  exmidpw  6865  djuf1olem  7009  fzen  9968  fihasheq0  10696  divalgb  11847  isprm3  12029  eldvap  13192