Metamath Proof Explorer


Theorem 3bitr4g

Description: More general version of 3bitr4i . Useful for converting definitions in a formula. (Contributed by NM, 11-May-1993)

Ref Expression
Hypotheses 3bitr4g.1
|- ( ph -> ( ps <-> ch ) )
3bitr4g.2
|- ( th <-> ps )
3bitr4g.3
|- ( ta <-> ch )
Assertion 3bitr4g
|- ( ph -> ( th <-> ta ) )

Proof

Step Hyp Ref Expression
1 3bitr4g.1
 |-  ( ph -> ( ps <-> ch ) )
2 3bitr4g.2
 |-  ( th <-> ps )
3 3bitr4g.3
 |-  ( ta <-> ch )
4 2 1 bitrid
 |-  ( ph -> ( th <-> ch ) )
5 4 3 bitr4di
 |-  ( ph -> ( th <-> ta ) )