Theorem mpjao3dan 1459

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 1458	. 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:  wemaplem2  9525  r1val1  9776  xleadd1a  13364  xlt2add  13371  xmullem  13375  xmulgt0  13394  xmulasslem3  13397  xlemul1a  13399  xadddilem  13405  xadddi  13406  xadddi2  13408  sgnmulsgn  15242  chnccat  18780  isxmet2d  24626  icccvx  25251  ivthicc  25759  mbfmulc2lem  25948  c1lip1  26297  dvivth  26310  reeff1o  26756  coseq00topi  26813  tanabsge  26817  logcnlem3  26954  atantan  27233  atanbnd  27236  cvxcl  27294  ostthlem1  27936  iscgrglt  28959  tgdim01ln  29009  lnxfr  29011  lnext  29012  tgfscgr  29013  tglineeltr  29081  colmid  29142  prodtp  33400  sgnmulsgp  33405  xrpxdivcld  33483  s3f1  33493  gsumtp  33607  cycpmco2  33676  cyc3co2  33683  archirngz  33732  archiabllem1b  33735  constrelextdg2  34361  constrfiss  34365  cos9thpiminplylem1  34396  esumcst  34677  hgt750lemb  35268  morleylemrneab  35283  weiunso  37224  exp11d  43351  fnwe2lem3  44012  chner  47839  crosspaltd  50910  crossp3d  50911