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  2001  sbal1  2002  dfsbcq2  2967  iindif2m  3956  opeqex  4251  rabxfrd  4471  eqbrrdv  4725  eqbrrdiv  4726  opelco2g  4797  opelcnvg  4809  ralrnmpt  5661  rexrnmpt  5662  fliftcnv  5799  eusvobj2  5864  f1od2  6239  ottposg  6259  ercnv  6559  exmidpw  6911  djuf1olem  7055  fzen  10046  fihasheq0  10776  divalgb  11933  isprm3  12121  eldvap  14291