Theorem mpjao3dan 1430

Description: Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) (Proof shortened by Wolf Lammen, 20-Apr-2024.)

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.4	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))
2		mpjao3dan.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		mpjao3dan.2	. . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4		mpjao3dan.3	. . 3 ⊢ ((𝜑 ∧ 𝜏) → 𝜒)
5	2, 3, 4	3jaodan 1429	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)
6	1, 5	mpdan 684	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∨ w3o 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088

This theorem is referenced by:  wemaplem2  9383  r1val1  9622  xleadd1a  13067  xlt2add  13074  xmullem  13078  xmulgt0  13097  xmulasslem3  13100  xlemul1a  13102  xadddilem  13108  xadddi  13109  xadddi2  13111  isxmet2d  23563  icccvx  24196  ivthicc  24705  mbfmulc2lem  24894  c1lip1  25244  dvivth  25257  reeff1o  25689  coseq00topi  25742  tanabsge  25746  logcnlem3  25882  atantan  26156  atanbnd  26159  cvxcl  26217  ostthlem1  26858  iscgrglt  27011  tgdim01ln  27061  lnxfr  27063  lnext  27064  tgfscgr  27065  tglineeltr  27128  colmid  27185  prodtp  31276  xrpxdivcld  31344  s3f1  31356  cycpmco2  31535  cyc3co2  31542  archirngz  31578  archiabllem1b  31581  esumcst  32171  sgnmulsgn  32656  sgnmulsgp  32657  hgt750lemb  32776  exp11d  40541  fnwe2lem3  41094