Theorem mpjao3dan 1343

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 715   ∨ w3o 1003

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 716

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

This theorem is referenced by:  wetriext  4675  nntri3  6665  nntri2or2  6666  nntr2  6671  tridc  7089  nnnninfeq  7327  exmidontriimlem2  7437  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprprlemnkj  7912  caucvgprprlemnbj  7913  caucvgsr  8022  npnflt  10050  nmnfgt  10053  xleadd1a  10108  xltadd1  10111  xlt2add  10115  xsubge0  10116  xleaddadd  10122  addmodlteq  10661  iseqf1olemkle  10760  hashfiv01gt1  11045  iswrdiz  11124  xrmaxltsup  11823  xrmaxadd  11826  xrbdtri  11841  cvgratz  12098  zdvdsdc  12378  divalglemeunn  12487  divalglemex  12488  divalglemeuneg  12489  divalg  12490  znege1  12755  ennnfonelemk  13026  isxmet2d  15078  trilpolemres  16672  trirec0  16674