Description: Theorem *3.22 of WhiteheadRussell p. 111. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 13-Nov-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | pm3.22 | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜓 ∧ 𝜑 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | ⊢ ( ( 𝜓 ∧ 𝜑 ) → ( 𝜓 ∧ 𝜑 ) ) | |
2 | 1 | ancoms | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜓 ∧ 𝜑 ) ) |