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  2029  sbal1  2030  dfsbcq2  3001  iindif2m  3995  opeqex  4295  rabxfrd  4517  eqbrrdv  4773  eqbrrdiv  4774  opelco2g  4847  opelcnvg  4859  ralrnmpt  5724  rexrnmpt  5725  fliftcnv  5866  eusvobj2  5932  f1od2  6323  ottposg  6343  ercnv  6643  exmidpw  7007  djuf1olem  7157  fzen  10167  fihasheq0  10940  divalgb  12269  isprm3  12473  eldvap  15187