Theorem mp2and

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

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

Proof

Step	Hyp	Ref	Expression
1		mp2and.1	|- ( ph -> ps )
2		mp2and.2	|- ( ph -> ch )
3		mp2and.3	|- ( ph -> ( ( ps /\ ch ) -> th ) )
4	1 3	mpand	|- ( ph -> ( ch -> th ) )
5	2 4	mpd	|- ( ph -> th )