Theorem 3bitr3g 220

Description: More general version of 3bitr3i 208. 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	syl5bbr 192	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3g.3	. 2 |- ( ch <-> ta )
5	3, 4	syl6bb 194	1 |- ( ph -> ( th <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  con2bidc  805  sbal1yz  1922  sbal1  1923  dfsbcq2  2832  iindif2m  3782  opeqex  4052  rabxfrd  4267  eqbrrdv  4505  eqbrrdiv  4506  opelco2g  4574  opelcnvg  4586  ralrnmpt  5406  rexrnmpt  5407  fliftcnv  5537  eusvobj2  5601  f1od2  5959  ottposg  5976  ercnv  6267  exmidpw  6578  djuf1olem  6692  fzen  9392  fihasheq0  10120  divalgb  10850  isprm3  11025