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  875  sbal1yz  1999  sbal1  2000  dfsbcq2  2963  iindif2m  3949  opeqex  4243  rabxfrd  4463  eqbrrdv  4717  eqbrrdiv  4718  opelco2g  4788  opelcnvg  4800  ralrnmpt  5650  rexrnmpt  5651  fliftcnv  5786  eusvobj2  5851  f1od2  6226  ottposg  6246  ercnv  6546  exmidpw  6898  djuf1olem  7042  fzen  10013  fihasheq0  10741  divalgb  11897  isprm3  12085  eldvap  13731