Theorem mpjao3dan 1318

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 709   ∨ w3o 979

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 710

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

This theorem is referenced by:  wetriext  4610  nntri3  6552  nntri2or2  6553  nntr2  6558  tridc  6957  nnnninfeq  7189  exmidontriimlem2  7284  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprprlemnkj  7754  caucvgprprlemnbj  7755  caucvgsr  7864  npnflt  9884  nmnfgt  9887  xleadd1a  9942  xltadd1  9945  xlt2add  9949  xsubge0  9950  xleaddadd  9956  addmodlteq  10472  iseqf1olemkle  10571  hashfiv01gt1  10856  iswrdiz  10924  xrmaxltsup  11404  xrmaxadd  11407  xrbdtri  11422  cvgratz  11678  zdvdsdc  11958  divalglemeunn  12065  divalglemex  12066  divalglemeuneg  12067  divalg  12068  znege1  12319  ennnfonelemk  12560  isxmet2d  14527  trilpolemres  15602  trirec0  15604