Theorem mpanr12

Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009)

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

Proof

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