Theorem mp3and

Description: A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		mp3and.1	|- ( ph -> ps )
2		mp3and.2	|- ( ph -> ch )
3		mp3and.3	|- ( ph -> th )
4		mp3and.4	|- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )
5	1 2 3	3jca	|- ( ph -> ( ps /\ ch /\ th ) )
6	5 4	mpd	|- ( ph -> ta )