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

Proof

Step	Hyp	Ref	Expression
1		pm2.61ii.1	⊢ ( ¬ 𝜑 → ( ¬ 𝜓 → 𝜒 ) )
2		pm2.61ii.2	⊢ ( 𝜑 → 𝜒 )
3		pm2.61ii.3	⊢ ( 𝜓 → 𝜒 )
4	1 3	pm2.61d2	⊢ ( ¬ 𝜑 → 𝜒 )
5	2 4	pm2.61i	⊢ 𝜒