Theorem mpjao3dan 1307

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 708   ∨ w3o 977

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 709

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

This theorem is referenced by:  wetriext  4578  nntri3  6500  nntri2or2  6501  nntr2  6506  tridc  6901  nnnninfeq  7128  exmidontriimlem2  7223  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprprlemnkj  7693  caucvgprprlemnbj  7694  caucvgsr  7803  npnflt  9817  nmnfgt  9820  xleadd1a  9875  xltadd1  9878  xlt2add  9882  xsubge0  9883  xleaddadd  9889  addmodlteq  10400  iseqf1olemkle  10486  hashfiv01gt1  10764  xrmaxltsup  11268  xrmaxadd  11271  xrbdtri  11286  cvgratz  11542  zdvdsdc  11821  divalglemeunn  11928  divalglemex  11929  divalglemeuneg  11930  divalg  11931  znege1  12180  ennnfonelemk  12403  isxmet2d  13887  trilpolemres  14829  trirec0  14831