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  9462  r1val1  9710  xleadd1a  13205  xlt2add  13212  xmullem  13216  xmulgt0  13235  xmulasslem3  13238  xlemul1a  13240  xadddilem  13246  xadddi  13247  xadddi2  13249  chnccat  18592  isxmet2d  24292  icccvx  24917  ivthicc  25425  mbfmulc2lem  25614  c1lip1  25964  dvivth  25977  reeff1o  26412  coseq00topi  26466  tanabsge  26470  logcnlem3  26608  atantan  26887  atanbnd  26890  cvxcl  26948  ostthlem1  27590  iscgrglt  28582  tgdim01ln  28632  lnxfr  28634  lnext  28635  tgfscgr  28636  tglineeltr  28699  colmid  28756  prodtp  32900  sgnmulsgn  32915  sgnmulsgp  32916  xrpxdivcld  32994  s3f1  33007  gsumtp  33125  cycpmco2  33194  cyc3co2  33201  archirngz  33250  archiabllem1b  33253  constrelextdg2  33891  constrfiss  33895  cos9thpiminplylem1  33926  esumcst  34207  hgt750lemb  34800  weiunso  36648  exp11d  42758  fnwe2lem3  43480  chner  47315