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  9523  r1val1  9772  xleadd1a  13309  xlt2add  13316  xmullem  13320  xmulgt0  13339  xmulasslem3  13342  xlemul1a  13344  xadddilem  13350  xadddi  13351  xadddi2  13353  sgnmulsgn  15186  chnccat  18720  isxmet2d  24559  icccvx  25184  ivthicc  25692  mbfmulc2lem  25881  c1lip1  26231  dvivth  26244  reeff1o  26690  coseq00topi  26747  tanabsge  26751  logcnlem3  26889  atantan  27168  atanbnd  27171  cvxcl  27229  ostthlem1  27871  iscgrglt  28864  tgdim01ln  28914  lnxfr  28916  lnext  28917  tgfscgr  28918  tglineeltr  28986  colmid  29047  prodtp  33305  sgnmulsgp  33310  xrpxdivcld  33388  s3f1  33398  gsumtp  33512  cycpmco2  33581  cyc3co2  33588  archirngz  33637  archiabllem1b  33640  constrelextdg2  34265  constrfiss  34269  cos9thpiminplylem1  34300  esumcst  34581  hgt750lemb  35172  morleylemrneab  35187  weiunso  37093  exp11d  43209  fnwe2lem3  43901  chner  47721  crosspaltd  50807  crossp3d  50808