Theorem mpjao3dan 1431

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 1430	. 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  9585  r1val1  9824  xleadd1a  13292  xlt2add  13299  xmullem  13303  xmulgt0  13322  xmulasslem3  13325  xlemul1a  13327  xadddilem  13333  xadddi  13334  xadddi2  13336  isxmet2d  24353  icccvx  24995  ivthicc  25507  mbfmulc2lem  25696  c1lip1  26051  dvivth  26064  reeff1o  26506  coseq00topi  26559  tanabsge  26563  logcnlem3  26701  atantan  26981  atanbnd  26984  cvxcl  27043  ostthlem1  27686  iscgrglt  28537  tgdim01ln  28587  lnxfr  28589  lnext  28590  tgfscgr  28591  tglineeltr  28654  colmid  28711  prodtp  32834  xrpxdivcld  32902  s3f1  32916  gsumtp  33044  cycpmco2  33136  cyc3co2  33143  archirngz  33179  archiabllem1b  33182  constrelextdg2  33752  esumcst  34044  sgnmulsgn  34531  sgnmulsgp  34532  hgt750lemb  34650  weiunso  36449  exp11d  42340  fnwe2lem3  43041