Metamath Proof Explorer


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 )