Theorem mpjao3dan 1266

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

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 680   ∨ w3o 942

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

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

This theorem is referenced by:  wetriext  4449  nntri3  6345  nntri2or2  6346  nntr2  6351  tridc  6744  caucvgprlemnkj  7416  caucvgprlemnbj  7417  caucvgprprlemnkj  7442  caucvgprprlemnbj  7443  caucvgsr  7538  npnflt  9485  nmnfgt  9488  xleadd1a  9543  xltadd1  9546  xlt2add  9550  xsubge0  9551  xleaddadd  9557  addmodlteq  10058  iseqf1olemkle  10144  hashfiv01gt1  10415  xrmaxltsup  10913  xrmaxadd  10916  xrbdtri  10931  cvgratz  11187  zdvdsdc  11356  divalglemeunn  11460  divalglemex  11461  divalglemeuneg  11462  divalg  11463  znege1  11695  ennnfonelemk  11752  isxmet2d  12331  nninfalllemn  12883  trilpolemres  12916