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 ( ( ( 𝜑𝜓 ) → ( 𝜒𝜃 ) ) → ( ( ( 𝜓𝜑 ) → ( 𝜃𝜒 ) ) → ( ( 𝜑𝜓 ) → ( 𝜒𝜃 ) ) ) )

Proof

Step Hyp Ref Expression
1 impbi ( ( 𝜒𝜃 ) → ( ( 𝜃𝜒 ) → ( 𝜒𝜃 ) ) )
2 1 bj-bi3ant ( ( ( 𝜑𝜓 ) → ( 𝜒𝜃 ) ) → ( ( ( 𝜓𝜑 ) → ( 𝜃𝜒 ) ) → ( ( 𝜑𝜓 ) → ( 𝜒𝜃 ) ) ) )