Theorem or32dd

Description: A rearrangement of disjuncts, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018)

	Ref	Expression
Hypothesis	or32dd.1	⊢ ( 𝜑 → ( 𝜓 → ( ( 𝜒 ∨ 𝜃 ) ∨ 𝜏 ) ) )
Assertion	or32dd	⊢ ( 𝜑 → ( 𝜓 → ( ( 𝜒 ∨ 𝜏 ) ∨ 𝜃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		or32dd.1	⊢ ( 𝜑 → ( 𝜓 → ( ( 𝜒 ∨ 𝜃 ) ∨ 𝜏 ) ) )
2		or32	⊢ ( ( ( 𝜒 ∨ 𝜏 ) ∨ 𝜃 ) ↔ ( ( 𝜒 ∨ 𝜃 ) ∨ 𝜏 ) )
3	1 2	imbitrrdi	⊢ ( 𝜑 → ( 𝜓 → ( ( 𝜒 ∨ 𝜏 ) ∨ 𝜃 ) ) )