Theorem 3bitr3g 211

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  con2bidc  769  sbal1yz  1877  sbal1  1878  dfsbcq2  2767  iindif2m  3724  opeqex  3986  rabxfrd  4201  eqbrrdv  4437  eqbrrdiv  4438  opelco2g  4503  opelcnvg  4515  ralrnmpt  5309  rexrnmpt  5310  fliftcnv  5435  eusvobj2  5498  ottposg  5870  ercnv  6127  fzen  8907