Theorem 3jaoian

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

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

Proof

Step	Hyp	Ref	Expression
1		3jaoian.1	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
2		3jaoian.2	$$⊢\left(\theta \wedge \psi \right)\to \chi$$
3		3jaoian.3	$$⊢\left(\tau \wedge \psi \right)\to \chi$$
4	1	ex	$$⊢\phi \to \left(\psi \to \chi \right)$$
5	2	ex	$$⊢\theta \to \left(\psi \to \chi \right)$$
6	3	ex	$$⊢\tau \to \left(\psi \to \chi \right)$$
7	4 5 6	3jaoi	$$⊢\left(\phi \vee \theta \vee \tau \right)\to \left(\psi \to \chi \right)$$
8	7	imp	$$⊢\left(\left(\phi \vee \theta \vee \tau \right)\wedge \psi \right)\to \chi$$