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  877  sbal1yz  2030  sbal1  2031  dfsbcq2  3008  iindif2m  4009  opeqex  4312  rabxfrd  4534  eqbrrdv  4790  eqbrrdiv  4791  opelco2g  4864  opelcnvg  4876  ralrnmpt  5745  rexrnmpt  5746  fliftcnv  5887  eusvobj2  5953  f1od2  6344  ottposg  6364  ercnv  6664  exmidpw  7031  djuf1olem  7181  fzen  10200  fihasheq0  10975  divalgb  12351  isprm3  12555  eldvap  15269