Theorem mpjao3dan 1455

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

Syntax hints:   → wi 4   ∧ wa 400   ∨ w3o 1100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103

This theorem is referenced by:  wemaplem2  9497  r1val1  9746  xleadd1a  13270  xlt2add  13277  xmullem  13281  xmulgt0  13300  xmulasslem3  13303  xlemul1a  13305  xadddilem  13311  xadddi  13312  xadddi2  13314  sgnmulsgn  15136  chnccat  18672  isxmet2d  24445  icccvx  25070  ivthicc  25578  mbfmulc2lem  25767  c1lip1  26117  dvivth  26130  reeff1o  26568  coseq00topi  26625  tanabsge  26629  logcnlem3  26767  atantan  27046  atanbnd  27049  cvxcl  27107  ostthlem1  27749  iscgrglt  28741  tgdim01ln  28791  lnxfr  28793  lnext  28794  tgfscgr  28795  tglineeltr  28858  colmid  28919  prodtp  33084  sgnmulsgp  33089  xrpxdivcld  33167  s3f1  33180  gsumtp  33297  cycpmco2  33366  cyc3co2  33373  archirngz  33422  archiabllem1b  33425  constrelextdg2  34054  constrfiss  34058  cos9thpiminplylem1  34089  esumcst  34370  hgt750lemb  34960  morleylemrneab  34975  weiunso  36839  exp11d  42947  fnwe2lem3  43641  chner  47459