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  9566  r1val1  9805  xleadd1a  13274  xlt2add  13281  xmullem  13285  xmulgt0  13304  xmulasslem3  13307  xlemul1a  13309  xadddilem  13315  xadddi  13316  xadddi2  13318  isxmet2d  24271  icccvx  24904  ivthicc  25416  mbfmulc2lem  25605  c1lip1  25959  dvivth  25972  reeff1o  26414  coseq00topi  26468  tanabsge  26472  logcnlem3  26610  atantan  26890  atanbnd  26893  cvxcl  26952  ostthlem1  27595  iscgrglt  28498  tgdim01ln  28548  lnxfr  28550  lnext  28551  tgfscgr  28552  tglineeltr  28615  colmid  28672  prodtp  32811  sgnmulsgn  32826  sgnmulsgp  32827  xrpxdivcld  32914  s3f1  32927  gsumtp  33057  cycpmco2  33149  cyc3co2  33156  archirngz  33192  archiabllem1b  33195  constrelextdg2  33786  constrfiss  33790  cos9thpiminplylem1  33821  esumcst  34099  hgt750lemb  34693  weiunso  36489  exp11d  42342  fnwe2lem3  43043