Theorem mpd3an23

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

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

Proof

Step	Hyp	Ref	Expression
1		mpd3an23.1	|- ( ph -> ps )
2		mpd3an23.2	|- ( ph -> ch )
3		mpd3an23.3	|- ( ( ph /\ ps /\ ch ) -> th )
4		id	|- ( ph -> ph )
5	4 1 2 3	syl3anc	|- ( ph -> th )