Theorem mpjao3dan 1451

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 1450	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)
6	1, 5	mpdan 697	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399   ∨ w3o 1096

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 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099

This theorem is referenced by:  wemaplem2  9492  r1val1  9741  xleadd1a  13253  xlt2add  13260  xmullem  13264  xmulgt0  13283  xmulasslem3  13286  xlemul1a  13288  xadddilem  13294  xadddi  13295  xadddi2  13297  chnccat  18641  isxmet2d  24367  icccvx  24992  ivthicc  25500  mbfmulc2lem  25689  c1lip1  26039  dvivth  26052  reeff1o  26487  coseq00topi  26544  tanabsge  26548  logcnlem3  26686  atantan  26965  atanbnd  26968  cvxcl  27026  ostthlem1  27668  iscgrglt  28660  tgdim01ln  28710  lnxfr  28712  lnext  28713  tgfscgr  28714  tglineeltr  28777  colmid  28834  prodtp  32979  sgnmulsgn  32994  sgnmulsgp  32995  xrpxdivcld  33073  s3f1  33086  gsumtp  33205  cycpmco2  33274  cyc3co2  33281  archirngz  33330  archiabllem1b  33333  constrelextdg2  34005  constrfiss  34009  cos9thpiminplylem1  34040  esumcst  34321  hgt750lemb  34914  morleylemrneab  34929  weiunso  36790  exp11d  42899  fnwe2lem3  43593  chner  47425