Theorem mpjao3dan 1430

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 1429	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)
6	1, 5	mpdan 684	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∨ 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 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088

This theorem is referenced by:  wemaplem2  9306  r1val1  9544  xleadd1a  12987  xlt2add  12994  xmullem  12998  xmulgt0  13017  xmulasslem3  13020  xlemul1a  13022  xadddilem  13028  xadddi  13029  xadddi2  13031  isxmet2d  23480  icccvx  24113  ivthicc  24622  mbfmulc2lem  24811  c1lip1  25161  dvivth  25174  reeff1o  25606  coseq00topi  25659  tanabsge  25663  logcnlem3  25799  atantan  26073  atanbnd  26076  cvxcl  26134  ostthlem1  26775  iscgrglt  26875  tgdim01ln  26925  lnxfr  26927  lnext  26928  tgfscgr  26929  tglineeltr  26992  colmid  27049  prodtp  31141  xrpxdivcld  31209  s3f1  31221  cycpmco2  31400  cyc3co2  31407  archirngz  31443  archiabllem1b  31446  esumcst  32031  sgnmulsgn  32516  sgnmulsgp  32517  hgt750lemb  32636  exp11d  40325  fnwe2lem3  40877