Theorem 3jaodan

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

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

Proof

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