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  9452  r1val1  9698  xleadd1a  13168  xlt2add  13175  xmullem  13179  xmulgt0  13198  xmulasslem3  13201  xlemul1a  13203  xadddilem  13209  xadddi  13210  xadddi2  13212  chnccat  18549  isxmet2d  24271  icccvx  24904  ivthicc  25415  mbfmulc2lem  25604  c1lip1  25958  dvivth  25971  reeff1o  26413  coseq00topi  26467  tanabsge  26471  logcnlem3  26609  atantan  26889  atanbnd  26892  cvxcl  26951  ostthlem1  27594  iscgrglt  28586  tgdim01ln  28636  lnxfr  28638  lnext  28639  tgfscgr  28640  tglineeltr  28703  colmid  28760  prodtp  32908  sgnmulsgn  32923  sgnmulsgp  32924  xrpxdivcld  33016  s3f1  33029  gsumtp  33147  cycpmco2  33215  cyc3co2  33222  archirngz  33271  archiabllem1b  33274  constrelextdg2  33904  constrfiss  33908  cos9thpiminplylem1  33939  esumcst  34220  hgt750lemb  34813  weiunso  36660  exp11d  42577  fnwe2lem3  43290  chner  47125