This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Propositional calculus Abbreviated conjunction and disjunction of three wff's 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 ⊢ ( 𝜑 → 𝜒 )