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  4613  nntri3  6555  nntri2or2  6556  nntr2  6561  tridc  6960  nnnninfeq  7194  exmidontriimlem2  7289  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprprlemnkj  7759  caucvgprprlemnbj  7760  caucvgsr  7869  npnflt  9890  nmnfgt  9893  xleadd1a  9948  xltadd1  9951  xlt2add  9955  xsubge0  9956  xleaddadd  9962  addmodlteq  10490  iseqf1olemkle  10589  hashfiv01gt1  10874  iswrdiz  10942  xrmaxltsup  11423  xrmaxadd  11426  xrbdtri  11441  cvgratz  11697  zdvdsdc  11977  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  divalg  12089  znege1  12346  ennnfonelemk  12617  isxmet2d  14584  trilpolemres  15686  trirec0  15688