Theorem mpjao3dan 1433

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085

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 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  wemaplem2  9588  r1val1  9827  xleadd1a  13296  xlt2add  13303  xmullem  13307  xmulgt0  13326  xmulasslem3  13329  xlemul1a  13331  xadddilem  13337  xadddi  13338  xadddi2  13340  isxmet2d  24338  icccvx  24982  ivthicc  25494  mbfmulc2lem  25683  c1lip1  26037  dvivth  26050  reeff1o  26492  coseq00topi  26545  tanabsge  26549  logcnlem3  26687  atantan  26967  atanbnd  26970  cvxcl  27029  ostthlem1  27672  iscgrglt  28523  tgdim01ln  28573  lnxfr  28575  lnext  28576  tgfscgr  28577  tglineeltr  28640  colmid  28697  prodtp  32830  xrpxdivcld  32918  s3f1  32932  gsumtp  33062  cycpmco2  33154  cyc3co2  33161  archirngz  33197  archiabllem1b  33200  constrelextdg2  33789  esumcst  34065  sgnmulsgn  34553  sgnmulsgp  34554  hgt750lemb  34672  weiunso  36468  exp11d  42366  fnwe2lem3  43069