Theorem mpanr2

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

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

Proof

Step	Hyp	Ref	Expression
1		mpanr2.1	|- ch
2		mpanr2.2	|- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	1	jctr	|- ( ps -> ( ps /\ ch ) )
4	3 2	sylan2	|- ( ( ph /\ ps ) -> th )