Theorem mpjao3dan 1432

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

Syntax hints:   → wi 4   ∧ wa 397   ∨ w3o 1087

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 398  df-or 847  df-3or 1089  df-3an 1090

This theorem is referenced by:  wemaplem2  9542  r1val1  9781  xleadd1a  13232  xlt2add  13239  xmullem  13243  xmulgt0  13262  xmulasslem3  13265  xlemul1a  13267  xadddilem  13273  xadddi  13274  xadddi2  13276  isxmet2d  23833  icccvx  24466  ivthicc  24975  mbfmulc2lem  25164  c1lip1  25514  dvivth  25527  reeff1o  25959  coseq00topi  26012  tanabsge  26016  logcnlem3  26152  atantan  26428  atanbnd  26431  cvxcl  26489  ostthlem1  27130  iscgrglt  27765  tgdim01ln  27815  lnxfr  27817  lnext  27818  tgfscgr  27819  tglineeltr  27882  colmid  27939  prodtp  32033  xrpxdivcld  32101  s3f1  32113  cycpmco2  32292  cyc3co2  32299  archirngz  32335  archiabllem1b  32338  esumcst  33061  sgnmulsgn  33548  sgnmulsgp  33549  hgt750lemb  33668  exp11d  41216  fnwe2lem3  41794