Theorem mpjao3dan 1320

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 710   ∨ w3o 980

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 711

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

This theorem is referenced by:  wetriext  4630  nntri3  6593  nntri2or2  6594  nntr2  6599  tridc  7008  nnnninfeq  7242  exmidontriimlem2  7347  caucvgprlemnkj  7792  caucvgprlemnbj  7793  caucvgprprlemnkj  7818  caucvgprprlemnbj  7819  caucvgsr  7928  npnflt  9950  nmnfgt  9953  xleadd1a  10008  xltadd1  10011  xlt2add  10015  xsubge0  10016  xleaddadd  10022  addmodlteq  10556  iseqf1olemkle  10655  hashfiv01gt1  10940  iswrdiz  11014  xrmaxltsup  11619  xrmaxadd  11622  xrbdtri  11637  cvgratz  11893  zdvdsdc  12173  divalglemeunn  12282  divalglemex  12283  divalglemeuneg  12284  divalg  12285  znege1  12550  ennnfonelemk  12821  isxmet2d  14870  trilpolemres  16096  trirec0  16098