Theorem jaoian

Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005)

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

Proof

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