Theorem mpjao3dan 1411

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

Syntax hints:   → wi 4   ∧ wa 387   ∨ wo 833   ∨ w3o 1067

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 199  df-an 388  df-or 834  df-3or 1069

This theorem is referenced by:  wemaplem2  8808  r1val1  9011  xleadd1a  12465  xlt2add  12472  xmullem  12476  xmulgt0  12495  xmulasslem3  12498  xlemul1a  12500  xadddilem  12506  xadddi  12507  xadddi2  12509  isxmet2d  22643  icccvx  23260  ivthicc  23765  mbfmulc2lem  23954  c1lip1  24300  dvivth  24313  reeff1o  24741  coseq00topi  24794  tanabsge  24798  logcnlem3  24931  atantan  25205  atanbnd  25208  cvxcl  25267  ostthlem1  25908  iscgrglt  26005  tgdim01ln  26055  lnxfr  26057  lnext  26058  tgfscgr  26059  tglineeltr  26122  colmid  26179  prodtp  30292  xrpxdivcld  30360  s3f1  30368  cyc3co2  30460  archirngz  30484  archiabllem1b  30487  esumcst  30966  sgnmulsgn  31453  sgnmulsgp  31454  hgt750lemb  31575  fnwe2lem3  39048