Theorem mpjao3dan 1434

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 1433	. 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  9500  r1val1  9739  xleadd1a  13213  xlt2add  13220  xmullem  13224  xmulgt0  13243  xmulasslem3  13246  xlemul1a  13248  xadddilem  13254  xadddi  13255  xadddi2  13257  isxmet2d  24215  icccvx  24848  ivthicc  25359  mbfmulc2lem  25548  c1lip1  25902  dvivth  25915  reeff1o  26357  coseq00topi  26411  tanabsge  26415  logcnlem3  26553  atantan  26833  atanbnd  26836  cvxcl  26895  ostthlem1  27538  iscgrglt  28441  tgdim01ln  28491  lnxfr  28493  lnext  28494  tgfscgr  28495  tglineeltr  28558  colmid  28615  prodtp  32752  sgnmulsgn  32767  sgnmulsgp  32768  xrpxdivcld  32855  s3f1  32868  gsumtp  32998  cycpmco2  33090  cyc3co2  33097  archirngz  33143  archiabllem1b  33146  constrelextdg2  33737  constrfiss  33741  cos9thpiminplylem1  33772  esumcst  34053  hgt750lemb  34647  weiunso  36454  exp11d  42314  fnwe2lem3  43041