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	|- ( -. ph -> ( -. ps -> ch ) )
	pm2.61ii.2	|- ( ph -> ch )
	pm2.61ii.3	|- ( ps -> ch )
Assertion	pm2.61ii	|- ch

Proof

Step	Hyp	Ref	Expression
1		pm2.61ii.1	|- ( -. ph -> ( -. ps -> ch ) )
2		pm2.61ii.2	|- ( ph -> ch )
3		pm2.61ii.3	|- ( ps -> ch )
4	1 3	pm2.61d2	|- ( -. ph -> ch )
5	2 4	pm2.61i	|- ch