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  1989  sbal1  1990  dfsbcq2  2954  iindif2m  3933  opeqex  4227  rabxfrd  4447  eqbrrdv  4701  eqbrrdiv  4702  opelco2g  4772  opelcnvg  4784  ralrnmpt  5627  rexrnmpt  5628  fliftcnv  5763  eusvobj2  5828  f1od2  6203  ottposg  6223  ercnv  6522  exmidpw  6874  djuf1olem  7018  fzen  9978  fihasheq0  10707  divalgb  11862  isprm3  12050  eldvap  13291