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  9464  r1val1  9710  xleadd1a  13180  xlt2add  13187  xmullem  13191  xmulgt0  13210  xmulasslem3  13213  xlemul1a  13215  xadddilem  13221  xadddi  13222  xadddi2  13224  chnccat  18561  isxmet2d  24283  icccvx  24916  ivthicc  25427  mbfmulc2lem  25616  c1lip1  25970  dvivth  25983  reeff1o  26425  coseq00topi  26479  tanabsge  26483  logcnlem3  26621  atantan  26901  atanbnd  26904  cvxcl  26963  ostthlem1  27606  iscgrglt  28598  tgdim01ln  28648  lnxfr  28650  lnext  28651  tgfscgr  28652  tglineeltr  28715  colmid  28772  prodtp  32918  sgnmulsgn  32933  sgnmulsgp  32934  xrpxdivcld  33026  s3f1  33039  gsumtp  33157  cycpmco2  33226  cyc3co2  33233  archirngz  33282  archiabllem1b  33285  constrelextdg2  33924  constrfiss  33928  cos9thpiminplylem1  33959  esumcst  34240  hgt750lemb  34833  weiunso  36679  exp11d  42690  fnwe2lem3  43403  chner  47237