Theorem mpjao3dan

Description: Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018) (Proof shortened by Wolf Lammen, 20-Apr-2024)

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

Proof

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