Theorem mp3an2ani

Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017)

	Ref	Expression
Hypotheses	mp3an2ani.1	|- ph
	mp3an2ani.2	|- ( ps -> ch )
	mp3an2ani.3	|- ( ( ps /\ th ) -> ta )
	mp3an2ani.4	|- ( ( ph /\ ch /\ ta ) -> et )
Assertion	mp3an2ani	|- ( ( ps /\ th ) -> et )

Proof

Step	Hyp	Ref	Expression
1		mp3an2ani.1	|- ph
2		mp3an2ani.2	|- ( ps -> ch )
3		mp3an2ani.3	|- ( ( ps /\ th ) -> ta )
4		mp3an2ani.4	|- ( ( ph /\ ch /\ ta ) -> et )
5	1 2 3 4	mp3an3an	|- ( ( ps /\ ( ps /\ th ) ) -> et )
6	5	anabss5	|- ( ( ps /\ th ) -> et )