Theorem mpjao3dan 1286

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

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 698   ∨ w3o 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116  df-3or 964

This theorem is referenced by:  wetriext  4530  nntri3  6433  nntri2or2  6434  nntr2  6439  tridc  6833  exmidontriimlem2  7136  caucvgprlemnkj  7565  caucvgprlemnbj  7566  caucvgprprlemnkj  7591  caucvgprprlemnbj  7592  caucvgsr  7701  npnflt  9697  nmnfgt  9700  xleadd1a  9755  xltadd1  9758  xlt2add  9762  xsubge0  9763  xleaddadd  9769  addmodlteq  10275  iseqf1olemkle  10361  hashfiv01gt1  10633  xrmaxltsup  11132  xrmaxadd  11135  xrbdtri  11150  cvgratz  11406  zdvdsdc  11681  divalglemeunn  11785  divalglemex  11786  divalglemeuneg  11787  divalg  11788  znege1  12024  ennnfonelemk  12088  isxmet2d  12695  nninfalllemn  13528  trilpolemres  13562  trirec0  13564