Theorem mpjaod

Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016)

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

Proof

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