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  9507  r1val1  9746  xleadd1a  13220  xlt2add  13227  xmullem  13231  xmulgt0  13250  xmulasslem3  13253  xlemul1a  13255  xadddilem  13261  xadddi  13262  xadddi2  13264  isxmet2d  24222  icccvx  24855  ivthicc  25366  mbfmulc2lem  25555  c1lip1  25909  dvivth  25922  reeff1o  26364  coseq00topi  26418  tanabsge  26422  logcnlem3  26560  atantan  26840  atanbnd  26843  cvxcl  26902  ostthlem1  27545  iscgrglt  28448  tgdim01ln  28498  lnxfr  28500  lnext  28501  tgfscgr  28502  tglineeltr  28565  colmid  28622  prodtp  32759  sgnmulsgn  32774  sgnmulsgp  32775  xrpxdivcld  32862  s3f1  32875  gsumtp  33005  cycpmco2  33097  cyc3co2  33104  archirngz  33150  archiabllem1b  33153  constrelextdg2  33744  constrfiss  33748  cos9thpiminplylem1  33779  esumcst  34060  hgt750lemb  34654  weiunso  36461  exp11d  42321  fnwe2lem3  43048