Theorem mpjao3dan 1434

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085

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 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  wemaplem2  9458  r1val1  9701  xleadd1a  13173  xlt2add  13180  xmullem  13184  xmulgt0  13203  xmulasslem3  13206  xlemul1a  13208  xadddilem  13214  xadddi  13215  xadddi2  13217  isxmet2d  24231  icccvx  24864  ivthicc  25375  mbfmulc2lem  25564  c1lip1  25918  dvivth  25931  reeff1o  26373  coseq00topi  26427  tanabsge  26431  logcnlem3  26569  atantan  26849  atanbnd  26852  cvxcl  26911  ostthlem1  27554  iscgrglt  28477  tgdim01ln  28527  lnxfr  28529  lnext  28530  tgfscgr  28531  tglineeltr  28594  colmid  28651  prodtp  32785  sgnmulsgn  32800  sgnmulsgp  32801  xrpxdivcld  32888  s3f1  32901  gsumtp  33024  cycpmco2  33088  cyc3co2  33095  archirngz  33144  archiabllem1b  33147  constrelextdg2  33716  constrfiss  33720  cos9thpiminplylem1  33751  esumcst  34032  hgt750lemb  34626  weiunso  36442  exp11d  42302  fnwe2lem3  43028