Theorem mpjao3dan 1341

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 713   ∨ w3o 1001

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 714

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

This theorem is referenced by:  wetriext  4673  nntri3  6660  nntri2or2  6661  nntr2  6666  tridc  7084  nnnninfeq  7321  exmidontriimlem2  7430  caucvgprlemnkj  7879  caucvgprlemnbj  7880  caucvgprprlemnkj  7905  caucvgprprlemnbj  7906  caucvgsr  8015  npnflt  10043  nmnfgt  10046  xleadd1a  10101  xltadd1  10104  xlt2add  10108  xsubge0  10109  xleaddadd  10115  addmodlteq  10653  iseqf1olemkle  10752  hashfiv01gt1  11037  iswrdiz  11113  xrmaxltsup  11812  xrmaxadd  11815  xrbdtri  11830  cvgratz  12086  zdvdsdc  12366  divalglemeunn  12475  divalglemex  12476  divalglemeuneg  12477  divalg  12478  znege1  12743  ennnfonelemk  13014  isxmet2d  15065  trilpolemres  16596  trirec0  16598