Theorem mpjao3dan 1297

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

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 698   ∨ w3o 967

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

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

This theorem is referenced by:  wetriext  4554  nntri3  6465  nntri2or2  6466  nntr2  6471  tridc  6865  nnnninfeq  7092  exmidontriimlem2  7178  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprprlemnkj  7633  caucvgprprlemnbj  7634  caucvgsr  7743  npnflt  9751  nmnfgt  9754  xleadd1a  9809  xltadd1  9812  xlt2add  9816  xsubge0  9817  xleaddadd  9823  addmodlteq  10333  iseqf1olemkle  10419  hashfiv01gt1  10695  xrmaxltsup  11199  xrmaxadd  11202  xrbdtri  11217  cvgratz  11473  zdvdsdc  11752  divalglemeunn  11858  divalglemex  11859  divalglemeuneg  11860  divalg  11861  znege1  12110  ennnfonelemk  12333  isxmet2d  12988  trilpolemres  13921  trirec0  13923