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  9433  r1val1  9679  xleadd1a  13152  xlt2add  13159  xmullem  13163  xmulgt0  13182  xmulasslem3  13185  xlemul1a  13187  xadddilem  13193  xadddi  13194  xadddi2  13196  chnccat  18532  isxmet2d  24243  icccvx  24876  ivthicc  25387  mbfmulc2lem  25576  c1lip1  25930  dvivth  25943  reeff1o  26385  coseq00topi  26439  tanabsge  26443  logcnlem3  26581  atantan  26861  atanbnd  26864  cvxcl  26923  ostthlem1  27566  iscgrglt  28493  tgdim01ln  28543  lnxfr  28545  lnext  28546  tgfscgr  28547  tglineeltr  28610  colmid  28667  prodtp  32808  sgnmulsgn  32823  sgnmulsgp  32824  xrpxdivcld  32913  s3f1  32926  gsumtp  33036  cycpmco2  33100  cyc3co2  33107  archirngz  33156  archiabllem1b  33159  constrelextdg2  33758  constrfiss  33762  cos9thpiminplylem1  33793  esumcst  34074  hgt750lemb  34667  weiunso  36506  exp11d  42365  fnwe2lem3  43091