Theorem mpjao3dan 1432

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ 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 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089

This theorem is referenced by:  wemaplem2  9616  r1val1  9855  xleadd1a  13315  xlt2add  13322  xmullem  13326  xmulgt0  13345  xmulasslem3  13348  xlemul1a  13350  xadddilem  13356  xadddi  13357  xadddi2  13359  isxmet2d  24358  icccvx  25000  ivthicc  25512  mbfmulc2lem  25701  c1lip1  26056  dvivth  26069  reeff1o  26509  coseq00topi  26562  tanabsge  26566  logcnlem3  26704  atantan  26984  atanbnd  26987  cvxcl  27046  ostthlem1  27689  iscgrglt  28540  tgdim01ln  28590  lnxfr  28592  lnext  28593  tgfscgr  28594  tglineeltr  28657  colmid  28714  prodtp  32831  xrpxdivcld  32899  s3f1  32913  gsumtp  33039  cycpmco2  33126  cyc3co2  33133  archirngz  33169  archiabllem1b  33172  constrelextdg2  33737  esumcst  34027  sgnmulsgn  34514  sgnmulsgp  34515  hgt750lemb  34633  weiunso  36432  exp11d  42313  fnwe2lem3  43009