Theorem mpjao3dan 1460

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105

This theorem is used by:  fnwe2lem4  8178  wemaplem2  9571  r1val1  9823  xleadd1a  13413  xlt2add  13420  xmullem  13424  xmulgt0  13443  xmulasslem3  13446  xlemul1a  13448  xadddilem  13454  xadddi  13455  xadddi2  13457  sgnmulsgn  15294  chnccat  18832  isxmet2d  24679  icccvx  25304  ivthicc  25812  mbfmulc2lem  26001  c1lip1  26350  dvivth  26363  reeff1o  26807  coseq00topi  26864  tanabsge  26868  logcnlem3  27005  atantan  27284  atanbnd  27287  cvxcl  27345  ostthlem1  27987  iscgrglt  29010  tgdim01ln  29060  lnxfr  29062  lnext  29063  tgfscgr  29064  tglineeltr  29132  colmid  29193  prodtp  33491  sgnmulsgp  33496  xrpxdivcld  33574  s3f1  33584  gsumtp  33701  cycpmco2  33770  cyc3co2  33777  archirngz  33826  archiabllem1b  33829  constrelextdg2  34462  constrfiss  34466  cos9thpiminplylem1  34497  esumcst  34778  hgt750lemb  35368  morleylemrneab  35383  weiunso  37445  exp11d  43587  chner  48110  crosspaltd  51278  crossp3d  51279