Theorem 3jaod

Description: Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005)

	Ref	Expression
Hypotheses	3jaod.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
	3jaod.2	$$⊢\phi \to \left(\theta \to \chi \right)$$
	3jaod.3	$$⊢\phi \to \left(\tau \to \chi \right)$$
Assertion	3jaod	$$⊢\phi \to \left(\left(\psi \vee \theta \vee \tau \right)\to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		3jaod.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2		3jaod.2	$$⊢\phi \to \left(\theta \to \chi \right)$$
3		3jaod.3	$$⊢\phi \to \left(\tau \to \chi \right)$$
4		3jao	$$⊢\left(\left(\psi \to \chi \right)\wedge \left(\theta \to \chi \right)\wedge \left(\tau \to \chi \right)\right)\to \left(\left(\psi \vee \theta \vee \tau \right)\to \chi \right)$$
5	1 2 3 4	syl3anc	$$⊢\phi \to \left(\left(\psi \vee \theta \vee \tau \right)\to \chi \right)$$