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  802  sbal1yz  1918  sbal1  1919  dfsbcq2  2818  iindif2m  3745  opeqex  4004  rabxfrd  4219  eqbrrdv  4455  eqbrrdiv  4456  opelco2g  4521  opelcnvg  4533  ralrnmpt  5330  rexrnmpt  5331  fliftcnv  5455  eusvobj2  5518  f1od2  5876  ottposg  5893  ercnv  6150  fzen  9062  divalgb  10325  isprm3  10500