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 φ ψ χ
mpjao3dan.2 φ θ χ
mpjao3dan.3 φ τ χ
mpjao3dan.4 φ ψ θ τ
Assertion mpjao3dan φ χ

Proof

Step Hyp Ref Expression
1 mpjao3dan.1 φ ψ χ
2 mpjao3dan.2 φ θ χ
3 mpjao3dan.3 φ τ χ
4 mpjao3dan.4 φ ψ θ τ
5 1 2 3 3jaodan φ ψ θ τ χ
6 4 5 mpdan φ χ