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 685	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394   ∨ 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 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086

This theorem is referenced by:  wemaplem2  9572  r1val1  9811  xleadd1a  13267  xlt2add  13274  xmullem  13278  xmulgt0  13297  xmulasslem3  13300  xlemul1a  13302  xadddilem  13308  xadddi  13309  xadddi2  13311  isxmet2d  24277  icccvx  24919  ivthicc  25431  mbfmulc2lem  25620  c1lip1  25974  dvivth  25987  reeff1o  26429  coseq00topi  26482  tanabsge  26486  logcnlem3  26623  atantan  26900  atanbnd  26903  cvxcl  26962  ostthlem1  27605  iscgrglt  28390  tgdim01ln  28440  lnxfr  28442  lnext  28443  tgfscgr  28444  tglineeltr  28507  colmid  28564  prodtp  32675  xrpxdivcld  32743  s3f1  32757  cycpmco2  32946  cyc3co2  32953  archirngz  32989  archiabllem1b  32992  esumcst  33810  sgnmulsgn  34297  sgnmulsgp  34298  hgt750lemb  34416  exp11d  42017  fnwe2lem3  42615