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 685	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∨ w3o 1086

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 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089

This theorem is referenced by:  wemaplem2  9544  r1val1  9783  xleadd1a  13234  xlt2add  13241  xmullem  13245  xmulgt0  13264  xmulasslem3  13267  xlemul1a  13269  xadddilem  13275  xadddi  13276  xadddi2  13278  isxmet2d  23840  icccvx  24473  ivthicc  24982  mbfmulc2lem  25171  c1lip1  25521  dvivth  25534  reeff1o  25966  coseq00topi  26019  tanabsge  26023  logcnlem3  26159  atantan  26435  atanbnd  26438  cvxcl  26496  ostthlem1  27137  iscgrglt  27803  tgdim01ln  27853  lnxfr  27855  lnext  27856  tgfscgr  27857  tglineeltr  27920  colmid  27977  prodtp  32071  xrpxdivcld  32139  s3f1  32151  cycpmco2  32333  cyc3co2  32340  archirngz  32376  archiabllem1b  32379  esumcst  33130  sgnmulsgn  33617  sgnmulsgp  33618  hgt750lemb  33737  exp11d  41298  fnwe2lem3  41876