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 699	1 ⊢ (𝜑 → 𝜒)

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

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

This theorem is referenced by:  wemaplem2  9510  r1val1  9759  xleadd1a  13280  xlt2add  13287  xmullem  13291  xmulgt0  13310  xmulasslem3  13313  xlemul1a  13315  xadddilem  13321  xadddi  13322  xadddi2  13324  sgnmulsgn  15148  chnccat  18683  isxmet2d  24465  icccvx  25090  ivthicc  25598  mbfmulc2lem  25787  c1lip1  26137  dvivth  26150  reeff1o  26591  coseq00topi  26648  tanabsge  26652  logcnlem3  26790  atantan  27069  atanbnd  27072  cvxcl  27130  ostthlem1  27772  iscgrglt  28764  tgdim01ln  28814  lnxfr  28816  lnext  28817  tgfscgr  28818  tglineeltr  28885  colmid  28946  prodtp  33152  sgnmulsgp  33157  xrpxdivcld  33235  s3f1  33248  gsumtp  33365  cycpmco2  33434  cyc3co2  33441  archirngz  33490  archiabllem1b  33493  constrelextdg2  34118  constrfiss  34122  cos9thpiminplylem1  34153  esumcst  34434  hgt750lemb  35024  morleylemrneab  35039  weiunso  36958  exp11d  43068  fnwe2lem3  43762  chner  47584