Theorem mp2ani

Description: An inference based on modus ponens. (Contributed by NM, 12-Dec-2004)

	Ref	Expression
Hypotheses	mp2ani.1	|- ps
	mp2ani.2	|- ch
	mp2ani.3	|- ( ph -> ( ( ps /\ ch ) -> th ) )
Assertion	mp2ani	|- ( ph -> th )

Proof

Step	Hyp	Ref	Expression
1		mp2ani.1	|- ps
2		mp2ani.2	|- ch
3		mp2ani.3	|- ( ph -> ( ( ps /\ ch ) -> th ) )
4	1 3	mpani	|- ( ph -> ( ch -> th ) )
5	2 4	mpi	|- ( ph -> th )