Metamath Proof Explorer


Theorem ancomst

Description: Closed form of ancoms . (Contributed by Alan Sare, 31-Dec-2011)

Ref Expression
Assertion ancomst ( ( ( 𝜑𝜓 ) → 𝜒 ) ↔ ( ( 𝜓𝜑 ) → 𝜒 ) )

Proof

Step Hyp Ref Expression
1 ancom ( ( 𝜑𝜓 ) ↔ ( 𝜓𝜑 ) )
2 1 imbi1i ( ( ( 𝜑𝜓 ) → 𝜒 ) ↔ ( ( 𝜓𝜑 ) → 𝜒 ) )