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  4576  nntri3  6497  nntri2or2  6498  nntr2  6503  tridc  6898  nnnninfeq  7125  exmidontriimlem2  7220  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprprlemnkj  7690  caucvgprprlemnbj  7691  caucvgsr  7800  npnflt  9814  nmnfgt  9817  xleadd1a  9872  xltadd1  9875  xlt2add  9879  xsubge0  9880  xleaddadd  9886  addmodlteq  10397  iseqf1olemkle  10483  hashfiv01gt1  10761  xrmaxltsup  11265  xrmaxadd  11268  xrbdtri  11283  cvgratz  11539  zdvdsdc  11818  divalglemeunn  11925  divalglemex  11926  divalglemeuneg  11927  divalg  11928  znege1  12177  ennnfonelemk  12400  isxmet2d  13818  trilpolemres  14760  trirec0  14762