Theorem mpjao3dan 1459

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 1458	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)
6	1, 5	mpdan 700	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ w3o 1102

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 402  df-or 862  df-3or 1104  df-3an 1105

This theorem is used by:  wemaplem2  9519  r1val1  9768  xleadd1a  13297  xlt2add  13304  xmullem  13308  xmulgt0  13327  xmulasslem3  13330  xlemul1a  13332  xadddilem  13338  xadddi  13339  xadddi2  13341  sgnmulsgn  15172  chnccat  18707  isxmet2d  24521  icccvx  25146  ivthicc  25654  mbfmulc2lem  25843  c1lip1  26193  dvivth  26206  reeff1o  26647  coseq00topi  26704  tanabsge  26708  logcnlem3  26846  atantan  27125  atanbnd  27128  cvxcl  27186  ostthlem1  27828  iscgrglt  28820  tgdim01ln  28870  lnxfr  28872  lnext  28873  tgfscgr  28874  tglineeltr  28941  colmid  29002  prodtp  33208  sgnmulsgp  33213  xrpxdivcld  33291  s3f1  33301  gsumtp  33415  cycpmco2  33484  cyc3co2  33491  archirngz  33540  archiabllem1b  33543  constrelextdg2  34168  constrfiss  34172  cos9thpiminplylem1  34203  esumcst  34484  hgt750lemb  35075  morleylemrneab  35090  weiunso  37018  exp11d  43128  fnwe2lem3  43820  chner  47642  crosspalti  50689  crossp3i  50690