Description: Theorem *2.32 of WhiteheadRussell p. 105. (Contributed by NM, 3-Jan-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | pm2.32 | ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) → ( 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orass | ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ↔ ( 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) ) | |
2 | 1 | biimpi | ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) → ( 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) ) |