Theorem 3bitr3g 221

Description: More general version of 3bitr3i 209. 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 193	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3g.3	. 2 |- ( ch <-> ta )
5	3, 4	bitrdi 195	1 |- ( ph -> ( th <-> ta ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  con2bidc  861  sbal1yz  1978  sbal1  1979  dfsbcq2  2936  iindif2m  3912  opeqex  4204  rabxfrd  4423  eqbrrdv  4676  eqbrrdiv  4677  opelco2g  4747  opelcnvg  4759  ralrnmpt  5602  rexrnmpt  5603  fliftcnv  5736  eusvobj2  5800  f1od2  6172  ottposg  6192  ercnv  6490  exmidpw  6842  djuf1olem  6983  fzen  9923  fihasheq0  10645  divalgb  11789  isprm3  11966  eldvap  12990