Theorem mpjao3dan 1307

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 708   ∨ w3o 977

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 709

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

This theorem is referenced by:  wetriext  4575  nntri3  6495  nntri2or2  6496  nntr2  6501  tridc  6896  nnnninfeq  7123  exmidontriimlem2  7218  caucvgprlemnkj  7662  caucvgprlemnbj  7663  caucvgprprlemnkj  7688  caucvgprprlemnbj  7689  caucvgsr  7798  npnflt  9811  nmnfgt  9814  xleadd1a  9869  xltadd1  9872  xlt2add  9876  xsubge0  9877  xleaddadd  9883  addmodlteq  10393  iseqf1olemkle  10479  hashfiv01gt1  10755  xrmaxltsup  11259  xrmaxadd  11262  xrbdtri  11277  cvgratz  11533  zdvdsdc  11812  divalglemeunn  11918  divalglemex  11919  divalglemeuneg  11920  divalg  11921  znege1  12170  ennnfonelemk  12393  isxmet2d  13719  trilpolemres  14650  trirec0  14652