Theorem mpjao3dan 1435

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 1434	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)
6	1, 5	mpdan 688	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 849  df-3or 1088  df-3an 1089

This theorem is referenced by:  wemaplem2  9455  r1val1  9701  xleadd1a  13196  xlt2add  13203  xmullem  13207  xmulgt0  13226  xmulasslem3  13229  xlemul1a  13231  xadddilem  13237  xadddi  13238  xadddi2  13240  chnccat  18583  isxmet2d  24302  icccvx  24927  ivthicc  25435  mbfmulc2lem  25624  c1lip1  25974  dvivth  25987  reeff1o  26425  coseq00topi  26479  tanabsge  26483  logcnlem3  26621  atantan  26900  atanbnd  26903  cvxcl  26962  ostthlem1  27604  iscgrglt  28596  tgdim01ln  28646  lnxfr  28648  lnext  28649  tgfscgr  28650  tglineeltr  28713  colmid  28770  prodtp  32915  sgnmulsgn  32930  sgnmulsgp  32931  xrpxdivcld  33009  s3f1  33022  gsumtp  33140  cycpmco2  33209  cyc3co2  33216  archirngz  33265  archiabllem1b  33268  constrelextdg2  33907  constrfiss  33911  cos9thpiminplylem1  33942  esumcst  34223  hgt750lemb  34816  weiunso  36664  exp11d  42772  fnwe2lem3  43498  chner  47331