Metamath Proof Explorer


Theorem or32

Description: A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion or32 ( ( ( 𝜑𝜓 ) ∨ 𝜒 ) ↔ ( ( 𝜑𝜒 ) ∨ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 orass ( ( ( 𝜑𝜓 ) ∨ 𝜒 ) ↔ ( 𝜑 ∨ ( 𝜓𝜒 ) ) )
2 or12 ( ( 𝜑 ∨ ( 𝜓𝜒 ) ) ↔ ( 𝜓 ∨ ( 𝜑𝜒 ) ) )
3 orcom ( ( 𝜓 ∨ ( 𝜑𝜒 ) ) ↔ ( ( 𝜑𝜒 ) ∨ 𝜓 ) )
4 1 2 3 3bitri ( ( ( 𝜑𝜓 ) ∨ 𝜒 ) ↔ ( ( 𝜑𝜒 ) ∨ 𝜓 ) )