Theorem mpjao3dan 1435

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

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

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 849  df-3or 1088  df-3an 1089

This theorem is referenced by:  wemaplem2  9456  r1val1  9702  xleadd1a  13172  xlt2add  13179  xmullem  13183  xmulgt0  13202  xmulasslem3  13205  xlemul1a  13207  xadddilem  13213  xadddi  13214  xadddi2  13216  chnccat  18553  isxmet2d  24275  icccvx  24908  ivthicc  25419  mbfmulc2lem  25608  c1lip1  25962  dvivth  25975  reeff1o  26417  coseq00topi  26471  tanabsge  26475  logcnlem3  26613  atantan  26893  atanbnd  26896  cvxcl  26955  ostthlem1  27598  iscgrglt  28569  tgdim01ln  28619  lnxfr  28621  lnext  28622  tgfscgr  28623  tglineeltr  28686  colmid  28743  prodtp  32889  sgnmulsgn  32904  sgnmulsgp  32905  xrpxdivcld  32997  s3f1  33010  gsumtp  33128  cycpmco2  33196  cyc3co2  33203  archirngz  33252  archiabllem1b  33255  constrelextdg2  33885  constrfiss  33889  cos9thpiminplylem1  33920  esumcst  34201  hgt750lemb  34794  weiunso  36641  exp11d  42623  fnwe2lem3  43336  chner  47171