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	⊢ ( ¬ 𝜑 → ( ¬ 𝜓 → ( ¬ 𝜒 → 𝜃 ) ) )
	pm2.61iii.2	⊢ ( 𝜑 → 𝜃 )
	pm2.61iii.3	⊢ ( 𝜓 → 𝜃 )
	pm2.61iii.4	⊢ ( 𝜒 → 𝜃 )
Assertion	pm2.61iii	⊢ 𝜃

Proof

Step	Hyp	Ref	Expression
1		pm2.61iii.1	⊢ ( ¬ 𝜑 → ( ¬ 𝜓 → ( ¬ 𝜒 → 𝜃 ) ) )
2		pm2.61iii.2	⊢ ( 𝜑 → 𝜃 )
3		pm2.61iii.3	⊢ ( 𝜓 → 𝜃 )
4		pm2.61iii.4	⊢ ( 𝜒 → 𝜃 )
5	2	a1d	⊢ ( 𝜑 → ( ¬ 𝜒 → 𝜃 ) )
6	3	a1d	⊢ ( 𝜓 → ( ¬ 𝜒 → 𝜃 ) )
7	1 5 6	pm2.61ii	⊢ ( ¬ 𝜒 → 𝜃 )
8	4 7	pm2.61i	⊢ 𝜃