Theorem mpjao3dan 1344

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 716   ∨ w3o 1004

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 717

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

This theorem is referenced by:  wetriext  4698  nntri3  6729  nntri2or2  6730  nntr2  6735  tridc  7156  nnnninfeq  7418  exmidontriimlem2  7528  caucvgprlemnkj  7980  caucvgprlemnbj  7981  caucvgprprlemnkj  8006  caucvgprprlemnbj  8007  caucvgsr  8116  npnflt  10147  nmnfgt  10150  xleadd1a  10205  xltadd1  10208  xlt2add  10212  xsubge0  10213  xleaddadd  10219  addmodlteq  10759  iseqf1olemkle  10858  hashfiv01gt1  11143  iswrdiz  11227  xrmaxltsup  11939  xrmaxadd  11942  xrbdtri  11957  cvgratz  12214  zdvdsdc  12494  divalglemeunn  12603  divalglemex  12604  divalglemeuneg  12605  divalg  12606  znege1  12871  ennnfonelemk  13143  isxmet2d  15205  trilpolemres  16818  trirec0  16820