Theorem 3bitr3g 222

Description: More general version of 3bitr3i 210. 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 194	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3g.3	. 2 |- ( ch <-> ta )
5	3, 4	bitrdi 196	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:  con2bidc  880  sbal1yz  2052  sbal1  2053  dfsbcq2  3031  iindif2m  4033  opeqex  4336  rabxfrd  4560  eqbrrdv  4816  eqbrrdiv  4817  opelco2g  4890  opelcnvg  4902  ralrnmpt  5777  rexrnmpt  5778  fliftcnv  5919  eusvobj2  5987  f1od2  6381  ottposg  6401  ercnv  6701  exmidpw  7070  djuf1olem  7220  fzen  10239  fihasheq0  11015  divalgb  12436  isprm3  12640  eldvap  15356