Description: A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 26-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | or32 | ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∨ 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orass | ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ↔ ( 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) ) | |
2 | or12 | ⊢ ( ( 𝜑 ∨ ( 𝜓 ∨ 𝜒 ) ) ↔ ( 𝜓 ∨ ( 𝜑 ∨ 𝜒 ) ) ) | |
3 | orcom | ⊢ ( ( 𝜓 ∨ ( 𝜑 ∨ 𝜒 ) ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∨ 𝜓 ) ) | |
4 | 1 2 3 | 3bitri | ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∨ 𝜓 ) ) |