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

Proof

Step	Hyp	Ref	Expression
1		pm2.61iii.1	|- ( -. ph -> ( -. ps -> ( -. ch -> th ) ) )
2		pm2.61iii.2	|- ( ph -> th )
3		pm2.61iii.3	|- ( ps -> th )
4		pm2.61iii.4	|- ( ch -> th )
5	2	a1d	|- ( ph -> ( -. ch -> th ) )
6	3	a1d	|- ( ps -> ( -. ch -> th ) )
7	1 5 6	pm2.61ii	|- ( -. ch -> th )
8	4 7	pm2.61i	|- th