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  883  sbal1yz  2057  sbal1  2058  dfsbcq2  3048  iindif2m  4064  opeqex  4371  rabxfrd  4595  eqbrrdv  4852  eqbrrdiv  4853  opelco2g  4928  opelcnvg  4940  ralrnmpt  5824  rexrnmpt  5825  fliftcnv  5974  eusvobj2  6044  f1od2  6444  ottposg  6499  ercnv  6801  exmidpw  7181  djuf1olem  7357  fzen  10397  fihasheq0  11181  divalgb  12636  isprm3  12840  eldvap  15673