Theorem mpjao3dan 1440

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ w3o 1091

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 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094

This theorem is referenced by:  wemaplem2  9459  r1val1  9708  xleadd1a  13203  xlt2add  13210  xmullem  13214  xmulgt0  13233  xmulasslem3  13236  xlemul1a  13238  xadddilem  13244  xadddi  13245  xadddi2  13247  chnccat  18590  isxmet2d  24317  icccvx  24942  ivthicc  25450  mbfmulc2lem  25639  c1lip1  25989  dvivth  26002  reeff1o  26437  coseq00topi  26491  tanabsge  26495  logcnlem3  26633  atantan  26912  atanbnd  26915  cvxcl  26973  ostthlem1  27615  iscgrglt  28607  tgdim01ln  28657  lnxfr  28659  lnext  28660  tgfscgr  28661  tglineeltr  28724  colmid  28781  prodtp  32926  sgnmulsgn  32941  sgnmulsgp  32942  xrpxdivcld  33020  s3f1  33033  gsumtp  33152  cycpmco2  33221  cyc3co2  33228  archirngz  33277  archiabllem1b  33280  constrelextdg2  33938  constrfiss  33942  cos9thpiminplylem1  33973  esumcst  34254  hgt750lemb  34847  weiunso  36701  exp11d  42810  fnwe2lem3  43504  chner  47337