Theorem pm2.61iii

Description: Inference eliminating three antecedents. (Contributed by NM, 2-Jan-2002) (Proof shortened by Wolf Lammen, 22-Sep-2013)

	Ref	Expression
Hypotheses	pm2.61iii.1	$$⊢\neg \phi \to \left(\neg \psi \to \left(\neg \chi \to \theta \right)\right)$$
	pm2.61iii.2	$$⊢\phi \to \theta$$
	pm2.61iii.3	$$⊢\psi \to \theta$$
	pm2.61iii.4	$$⊢\chi \to \theta$$
Assertion	pm2.61iii	$$⊢\theta$$

Proof

Step	Hyp	Ref	Expression
1		pm2.61iii.1	$$⊢\neg \phi \to \left(\neg \psi \to \left(\neg \chi \to \theta \right)\right)$$
2		pm2.61iii.2	$$⊢\phi \to \theta$$
3		pm2.61iii.3	$$⊢\psi \to \theta$$
4		pm2.61iii.4	$$⊢\chi \to \theta$$
5	2	a1d	$$⊢\phi \to \left(\neg \chi \to \theta \right)$$
6	3	a1d	$$⊢\psi \to \left(\neg \chi \to \theta \right)$$
7	1 5 6	pm2.61ii	$$⊢\neg \chi \to \theta$$
8	4 7	pm2.61i	$$⊢\theta$$