Theorem mpjao3dan 1429

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1084

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 396  df-or 844  df-3or 1086  df-3an 1087

This theorem is referenced by:  wemaplem2  9236  r1val1  9475  xleadd1a  12916  xlt2add  12923  xmullem  12927  xmulgt0  12946  xmulasslem3  12949  xlemul1a  12951  xadddilem  12957  xadddi  12958  xadddi2  12960  isxmet2d  23388  icccvx  24019  ivthicc  24527  mbfmulc2lem  24716  c1lip1  25066  dvivth  25079  reeff1o  25511  coseq00topi  25564  tanabsge  25568  logcnlem3  25704  atantan  25978  atanbnd  25981  cvxcl  26039  ostthlem1  26680  iscgrglt  26779  tgdim01ln  26829  lnxfr  26831  lnext  26832  tgfscgr  26833  tglineeltr  26896  colmid  26953  prodtp  31043  xrpxdivcld  31111  s3f1  31123  cycpmco2  31302  cyc3co2  31309  archirngz  31345  archiabllem1b  31348  esumcst  31931  sgnmulsgn  32416  sgnmulsgp  32417  hgt750lemb  32536  exp11d  40246  fnwe2lem3  40793