Theorem mpjao3dan 1341

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 713   ∨ w3o 1001

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 714

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

This theorem is referenced by:  wetriext  4666  nntri3  6633  nntri2or2  6634  nntr2  6639  tridc  7049  nnnninfeq  7283  exmidontriimlem2  7392  caucvgprlemnkj  7841  caucvgprlemnbj  7842  caucvgprprlemnkj  7867  caucvgprprlemnbj  7868  caucvgsr  7977  npnflt  9999  nmnfgt  10002  xleadd1a  10057  xltadd1  10060  xlt2add  10064  xsubge0  10065  xleaddadd  10071  addmodlteq  10607  iseqf1olemkle  10706  hashfiv01gt1  10991  iswrdiz  11065  xrmaxltsup  11755  xrmaxadd  11758  xrbdtri  11773  cvgratz  12029  zdvdsdc  12309  divalglemeunn  12418  divalglemex  12419  divalglemeuneg  12420  divalg  12421  znege1  12686  ennnfonelemk  12957  isxmet2d  15007  trilpolemres  16341  trirec0  16343