Theorem mpjao3dan 1543

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 948	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
4		mpjao3dan.3	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜒)
5		mpjao3dan.4	. . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))
6		df-3or 1072	. . 3 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜏))
7	5, 6	sylib 208	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ∨ 𝜏))
8	3, 4, 7	mpjaodan 949	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 382   ∨ wo 826   ∨ w3o 1070

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 197  df-an 383  df-or 827  df-3or 1072

This theorem is referenced by:  wemaplem2  8607  r1val1  8812  xleadd1a  12287  xlt2add  12294  xmullem  12298  xmulgt0  12317  xmulasslem3  12320  xlemul1a  12322  xadddilem  12328  xadddi  12329  xadddi2  12331  isxmet2d  22351  icccvx  22968  ivthicc  23445  mbfmulc2lem  23633  c1lip1  23979  dvivth  23992  reeff1o  24420  coseq00topi  24474  tanabsge  24478  logcnlem3  24610  atantan  24870  atanbnd  24873  cvxcl  24931  ostthlem1  25536  iscgrglt  25629  tgdim01ln  25679  lnxfr  25681  lnext  25682  tgfscgr  25683  tglineeltr  25746  colmid  25803  prodtp  29910  xrpxdivcld  29980  archirngz  30080  archiabllem1b  30083  esumcst  30462  sgnmulsgn  30948  sgnmulsgp  30949  hgt750lemb  31071  fnwe2lem3  38144