Theorem mpjao3dan 1344

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 716   ∨ w3o 1004

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 717

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

This theorem is referenced by:  wetriext  4704  nntri3  6743  nntri2or2  6744  nntr2  6749  tridc  7170  nnnninfeq  7432  exmidontriimlem2  7542  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprprlemnkj  8023  caucvgprprlemnbj  8024  caucvgsr  8133  npnflt  10167  nmnfgt  10170  xleadd1a  10225  xltadd1  10228  xlt2add  10232  xsubge0  10233  xleaddadd  10239  addmodlteq  10784  iseqf1olemkle  10883  hashfiv01gt1  11170  iswrdiz  11256  xrmaxltsup  11968  xrmaxadd  11971  xrbdtri  11986  cvgratz  12243  zdvdsdc  12523  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  divalg  12635  znege1  12900  ennnfonelemk  13235  isxmet2d  15325  trilpolemres  16938  trirec0  16940