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  876  sbal1yz  2017  sbal1  2018  dfsbcq2  2989  iindif2m  3981  opeqex  4279  rabxfrd  4501  eqbrrdv  4757  eqbrrdiv  4758  opelco2g  4831  opelcnvg  4843  ralrnmpt  5701  rexrnmpt  5702  fliftcnv  5839  eusvobj2  5905  f1od2  6290  ottposg  6310  ercnv  6610  exmidpw  6966  djuf1olem  7114  fzen  10112  fihasheq0  10867  divalgb  12069  isprm3  12259  eldvap  14861