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  2055  sbal1  2056  dfsbcq2  3045  iindif2m  4059  opeqex  4366  rabxfrd  4590  eqbrrdv  4847  eqbrrdiv  4848  opelco2g  4923  opelcnvg  4935  ralrnmpt  5819  rexrnmpt  5820  fliftcnv  5968  eusvobj2  6036  f1od2  6431  ottposg  6486  ercnv  6788  exmidpw  7168  djuf1olem  7344  fzen  10377  fihasheq0  11156  divalgb  12611  isprm3  12815  eldvap  15547