Metamath Proof Explorer

Theorem bj-imbi12

Description: Uncurried (imported) form of imbi12 . (Contributed by BJ, 6-May-2019)

Ref Expression
Assertion bj-imbi12 
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ( ph -> ch ) <-> ( ps -> th ) ) )

Proof

Step Hyp Ref Expression
1 imbi12 
 |-  ( ( ph <-> ps ) -> ( ( ch <-> th ) -> ( ( ph -> ch ) <-> ( ps -> th ) ) ) )
2 1 imp 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ( ph -> ch ) <-> ( ps -> th ) ) )