Theorem mp4an

Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010)

	Ref	Expression
Hypotheses	mp4an.1	|- ph
	mp4an.2	|- ps
	mp4an.3	|- ch
	mp4an.4	|- th
	mp4an.5	|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
Assertion	mp4an	|- ta

Proof

Step	Hyp	Ref	Expression
1		mp4an.1	|- ph
2		mp4an.2	|- ps
3		mp4an.3	|- ch
4		mp4an.4	|- th
5		mp4an.5	|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
6	1 2	pm3.2i	|- ( ph /\ ps )
7	3 4	pm3.2i	|- ( ch /\ th )
8	6 7 5	mp2an	|- ta