Theorem mpjao3dan 1348

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 720   ∨ w3o 1008

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 721

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

This theorem is referenced by:  wetriext  4722  nntri3  6764  nntri2or2  6765  nntr2  6770  tridc  7198  nnnninfeq  7462  exmidontriimlem2  7572  caucvgprlemnkj  8027  caucvgprlemnbj  8028  caucvgprprlemnkj  8053  caucvgprprlemnbj  8054  caucvgsr  8163  npnflt  10200  nmnfgt  10203  xleadd1a  10258  xltadd1  10261  xlt2add  10265  xsubge0  10266  xleaddadd  10272  addmodlteq  10818  iseqf1olemkle  10917  hashfiv01gt1  11204  iswrdiz  11294  xrmaxltsup  12007  xrmaxadd  12010  xrbdtri  12025  cvgratz  12282  zdvdsdc  12562  divalglemeunn  12671  divalglemex  12672  divalglemeuneg  12673  divalg  12674  znege1  12939  ennnfonelemk  13274  isxmet2d  15432  trilpolemres  17065  trirec0  17067