Theorem mpjao3dan 1344

Description: Eliminate a 3-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 805	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
4		mpjao3dan.3	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜒)
5		mpjao3dan.4	. . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))
6		df-3or 1006	. . 3 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜏))
7	5, 6	sylib 122	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ∨ 𝜏))
8	3, 4, 7	mpjaodan 806	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 716   ∨ w3o 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717

This theorem depends on definitions:  df-bi 117  df-3or 1006

This theorem is referenced by:  wetriext  4704  nntri3  6743  nntri2or2  6744  nntr2  6749  tridc  7170  nnnninfeq  7432  exmidontriimlem2  7542  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprprlemnkj  8023  caucvgprprlemnbj  8024  caucvgsr  8133  npnflt  10170  nmnfgt  10173  xleadd1a  10228  xltadd1  10231  xlt2add  10235  xsubge0  10236  xleaddadd  10242  addmodlteq  10787  iseqf1olemkle  10886  hashfiv01gt1  11173  iswrdiz  11259  xrmaxltsup  11972  xrmaxadd  11975  xrbdtri  11990  cvgratz  12247  zdvdsdc  12527  divalglemeunn  12636  divalglemex  12637  divalglemeuneg  12638  divalg  12639  znege1  12904  ennnfonelemk  13239  isxmet2d  15343  trilpolemres  16966  trirec0  16968