Theorem mpjao3dan 1428

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

Syntax hints:   → wi 4   ∧ wa 399   ∨ w3o 1083

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 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086

This theorem is referenced by:  wemaplem2  8995  r1val1  9199  xleadd1a  12634  xlt2add  12641  xmullem  12645  xmulgt0  12664  xmulasslem3  12667  xlemul1a  12669  xadddilem  12675  xadddi  12676  xadddi2  12678  isxmet2d  22934  icccvx  23555  ivthicc  24062  mbfmulc2lem  24251  c1lip1  24600  dvivth  24613  reeff1o  25042  coseq00topi  25095  tanabsge  25099  logcnlem3  25235  atantan  25509  atanbnd  25512  cvxcl  25570  ostthlem1  26211  iscgrglt  26308  tgdim01ln  26358  lnxfr  26360  lnext  26361  tgfscgr  26362  tglineeltr  26425  colmid  26482  prodtp  30569  xrpxdivcld  30637  s3f1  30649  cycpmco2  30825  cyc3co2  30832  archirngz  30868  archiabllem1b  30871  esumcst  31432  sgnmulsgn  31917  sgnmulsgp  31918  hgt750lemb  32037  fnwe2lem3  39996