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  4609  nntri3  6550  nntri2or2  6551  nntr2  6556  tridc  6955  nnnninfeq  7187  exmidontriimlem2  7282  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprprlemnkj  7752  caucvgprprlemnbj  7753  caucvgsr  7862  npnflt  9881  nmnfgt  9884  xleadd1a  9939  xltadd1  9942  xlt2add  9946  xsubge0  9947  xleaddadd  9953  addmodlteq  10469  iseqf1olemkle  10568  hashfiv01gt1  10853  iswrdiz  10921  xrmaxltsup  11401  xrmaxadd  11404  xrbdtri  11419  cvgratz  11675  zdvdsdc  11955  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  divalg  12065  znege1  12316  ennnfonelemk  12557  isxmet2d  14516  trilpolemres  15532  trirec0  15534