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:  fnwe2lem4  8151  wemaplem2  9545  r1val1  9797  xleadd1a  13387  xlt2add  13394  xmullem  13398  xmulgt0  13417  xmulasslem3  13420  xlemul1a  13422  xadddilem  13428  xadddi  13429  xadddi2  13431  sgnmulsgn  15268  chnccat  18806  isxmet2d  24652  icccvx  25277  ivthicc  25785  mbfmulc2lem  25974  c1lip1  26323  dvivth  26336  reeff1o  26780  coseq00topi  26837  tanabsge  26841  logcnlem3  26978  atantan  27257  atanbnd  27260  cvxcl  27318  ostthlem1  27960  iscgrglt  28983  tgdim01ln  29033  lnxfr  29035  lnext  29036  tgfscgr  29037  tglineeltr  29105  colmid  29166  prodtp  33465  sgnmulsgp  33470  xrpxdivcld  33548  s3f1  33558  gsumtp  33672  cycpmco2  33741  cyc3co2  33748  archirngz  33797  archiabllem1b  33800  constrelextdg2  34426  constrfiss  34430  cos9thpiminplylem1  34461  esumcst  34742  hgt750lemb  35332  morleylemrneab  35347  weiunso  37347  exp11d  43477  chner  47989  crosspaltd  51135  crossp3d  51136