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  4669  nntri3  6651  nntri2or2  6652  nntr2  6657  tridc  7069  nnnninfeq  7303  exmidontriimlem2  7412  caucvgprlemnkj  7861  caucvgprlemnbj  7862  caucvgprprlemnkj  7887  caucvgprprlemnbj  7888  caucvgsr  7997  npnflt  10019  nmnfgt  10022  xleadd1a  10077  xltadd1  10080  xlt2add  10084  xsubge0  10085  xleaddadd  10091  addmodlteq  10628  iseqf1olemkle  10727  hashfiv01gt1  11012  iswrdiz  11086  xrmaxltsup  11777  xrmaxadd  11780  xrbdtri  11795  cvgratz  12051  zdvdsdc  12331  divalglemeunn  12440  divalglemex  12441  divalglemeuneg  12442  divalg  12443  znege1  12708  ennnfonelemk  12979  isxmet2d  15030  trilpolemres  16440  trirec0  16442