Theorem mpjao3dan 1387

Description: Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.)

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.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		mpjao3dan.2	. . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
3	1, 2	jaodan 822	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
4		mpjao3dan.3	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜒)
5		mpjao3dan.4	. . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))
6		df-3or 1032	. . 3 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜏))
7	5, 6	sylib 207	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ∨ 𝜏))
8	3, 4, 7	mpjaodan 823	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∨ wo 382   ∧ wa 383   ∨ w3o 1030

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 196  df-or 384  df-an 385  df-3or 1032

This theorem is referenced by:  wemaplem2  8335  r1val1  8532  xleadd1a  11955  xlt2add  11962  xmullem  11966  xmulgt0  11985  xmulasslem3  11988  xlemul1a  11990  xadddilem  11996  xadddi  11997  xadddi2  11999  isxmet2d  21942  icccvx  22557  ivthicc  23034  mbfmulc2lem  23220  c1lip1  23564  dvivth  23577  reeff1o  24005  coseq00topi  24058  tanabsge  24062  logcnlem3  24190  atantan  24450  atanbnd  24453  cvxcl  24511  ostthlem1  25116  iscgrglt  25209  tgdim01ln  25259  lnxfr  25261  lnext  25262  tgfscgr  25263  tglineeltr  25326  colmid  25383  xrpxdivcld  28974  archirngz  29074  archiabllem1b  29077  esumcst  29452  sgnmulsgn  29938  sgnmulsgp  29939  fnwe2lem3  36640