Metamath Proof Explorer


Theorem bj-bisym

Description: This used to be in the main part. (Contributed by Wolf Lammen, 14-May-2013) (Revised by BJ, 14-Jun-2019)

Ref Expression
Assertion bj-bisym
|- ( ( ( ph -> ps ) -> ( ch -> th ) ) -> ( ( ( ps -> ph ) -> ( th -> ch ) ) -> ( ( ph <-> ps ) -> ( ch <-> th ) ) ) )

Proof

Step Hyp Ref Expression
1 impbi
 |-  ( ( ch -> th ) -> ( ( th -> ch ) -> ( ch <-> th ) ) )
2 1 bj-bi3ant
 |-  ( ( ( ph -> ps ) -> ( ch -> th ) ) -> ( ( ( ps -> ph ) -> ( th -> ch ) ) -> ( ( ph <-> ps ) -> ( ch <-> th ) ) ) )