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

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:  con2bidc  887  sbal1yz  2061  sbal1  2062  dfsbcq2  3054  iindif2m  4080  opeqex  4390  rabxfrd  4615  eqbrrdv  4872  eqbrrdiv  4873  opelco2g  4948  opelcnvg  4960  ralrnmpt  5850  rexrnmpt  5851  fliftcnv  6001  eusvobj2  6071  f1od2  6471  ottposg  6526  ercnv  6828  exmidpw  7215  djuf1olem  7393  fzen  10447  fihasheq0  11232  divalgb  12692  isprm3  12896  eldvap  15783