Description: Closed form of ancoms . (Contributed by Alan Sare, 31-Dec-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | ancomst | ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ↔ ( ( 𝜓 ∧ 𝜑 ) → 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom | ⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜓 ∧ 𝜑 ) ) | |
2 | 1 | imbi1i | ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ↔ ( ( 𝜓 ∧ 𝜑 ) → 𝜒 ) ) |