Theorem pm2.61ii

Description: Inference eliminating two antecedents. (Contributed by NM, 4-Jan-1993) (Proof shortened by Josh Purinton, 29-Dec-2000)

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

Proof

Step	Hyp	Ref	Expression
1		pm2.61ii.1	$$⊢\neg \phi \to \left(\neg \psi \to \chi \right)$$
2		pm2.61ii.2	$$⊢\phi \to \chi$$
3		pm2.61ii.3	$$⊢\psi \to \chi$$
4	1 3	pm2.61d2	$$⊢\neg \phi \to \chi$$
5	2 4	pm2.61i	$$⊢\chi$$