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  11121  xrmaxltsup  11820  xrmaxadd  11823  xrbdtri  11838  cvgratz  12095  zdvdsdc  12375  divalglemeunn  12484  divalglemex  12485  divalglemeuneg  12486  divalg  12487  znege1  12752  ennnfonelemk  13023  isxmet2d  15075  trilpolemres  16667  trirec0  16669