Theorem or32dd

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

	Ref	Expression
Hypothesis	or32dd.1	$$⊢\phi \to \left(\psi \to \left(\left(\chi \vee \theta \right)\vee \tau \right)\right)$$
Assertion	or32dd	$$⊢\phi \to \left(\psi \to \left(\left(\chi \vee \tau \right)\vee \theta \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		or32dd.1	$$⊢\phi \to \left(\psi \to \left(\left(\chi \vee \theta \right)\vee \tau \right)\right)$$
2		or32	$$⊢\left(\left(\chi \vee \tau \right)\vee \theta \right)\leftrightarrow \left(\left(\chi \vee \theta \right)\vee \tau \right)$$
3	1 2	imbitrrdi	$$⊢\phi \to \left(\psi \to \left(\left(\chi \vee \tau \right)\vee \theta \right)\right)$$