Theorem mpanr1

Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994) (Proof shortened by Andrew Salmon, 7-May-2011)

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

Proof

Step	Hyp	Ref	Expression
1		mpanr1.1	|- ps
2		mpanr1.2	|- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	anassrs	|- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1 3	mpanl2	|- ( ( ph /\ ch ) -> th )