Theorem mpjaodan

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule \/ E ( \/ elimination), see natded . (Contributed by Mario Carneiro, 29-May-2016)

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

Proof

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