Theorem mpjao3dan 1458

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

Hypotheses

Ref	Expression
mpjao3dan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
mpjao3dan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)
mpjao3dan.3	⊢ ((𝜑 ∧ 𝜏) → 𝜒)
mpjao3dan.4	⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))

Assertion

Ref	Expression
mpjao3dan	⊢ (𝜑 → 𝜒)

Proof of Theorem mpjao3dan

Step	Hyp	Ref	Expression
1		mpjao3dan.4	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))
2		mpjao3dan.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		mpjao3dan.2	. . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4		mpjao3dan.3	. . 3 ⊢ ((𝜑 ∧ 𝜏) → 𝜒)
5	2, 3, 4	3jaodan 1457	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)
6	1, 5	mpdan 699	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∨ w3o 1101

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104

This theorem is used by:  wemaplem2  9507  r1val1  9756  xleadd1a  13285  xlt2add  13292  xmullem  13296  xmulgt0  13315  xmulasslem3  13318  xlemul1a  13320  xadddilem  13326  xadddi  13327  xadddi2  13329  sgnmulsgn  15153  chnccat  18688  isxmet2d  24495  icccvx  25120  ivthicc  25628  mbfmulc2lem  25817  c1lip1  26167  dvivth  26180  reeff1o  26621  coseq00topi  26678  tanabsge  26682  logcnlem3  26820  atantan  27099  atanbnd  27102  cvxcl  27160  ostthlem1  27802  iscgrglt  28794  tgdim01ln  28844  lnxfr  28846  lnext  28847  tgfscgr  28848  tglineeltr  28915  colmid  28976  prodtp  33182  sgnmulsgp  33187  xrpxdivcld  33265  s3f1  33276  gsumtp  33393  cycpmco2  33462  cyc3co2  33469  archirngz  33518  archiabllem1b  33521  constrelextdg2  34146  constrfiss  34150  cos9thpiminplylem1  34181  esumcst  34462  hgt750lemb  35052  morleylemrneab  35067  weiunso  37005  exp11d  43115  fnwe2lem3  43807  chner  47629  crosspalti  50675  crossp3i  50676