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 942	. 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 943	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 382   ∨ wo 836   ∨ 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 837  df-3or 1072

This theorem is referenced by:  wemaplem2  8612  r1val1  8817  xleadd1a  12288  xlt2add  12295  xmullem  12299  xmulgt0  12318  xmulasslem3  12321  xlemul1a  12323  xadddilem  12329  xadddi  12330  xadddi2  12332  isxmet2d  22352  icccvx  22969  ivthicc  23446  mbfmulc2lem  23634  c1lip1  23980  dvivth  23993  reeff1o  24421  coseq00topi  24475  tanabsge  24479  logcnlem3  24611  atantan  24871  atanbnd  24874  cvxcl  24932  ostthlem1  25537  iscgrglt  25630  tgdim01ln  25680  lnxfr  25682  lnext  25683  tgfscgr  25684  tglineeltr  25747  colmid  25804  prodtp  29913  xrpxdivcld  29983  archirngz  30083  archiabllem1b  30086  esumcst  30465  sgnmulsgn  30951  sgnmulsgp  30952  hgt750lemb  31074  fnwe2lem3  38148