Theorem mpjao3dan 1434

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ 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 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  wemaplem2  9440  r1val1  9686  xleadd1a  13154  xlt2add  13161  xmullem  13165  xmulgt0  13184  xmulasslem3  13187  xlemul1a  13189  xadddilem  13195  xadddi  13196  xadddi2  13198  chnccat  18534  isxmet2d  24243  icccvx  24876  ivthicc  25387  mbfmulc2lem  25576  c1lip1  25930  dvivth  25943  reeff1o  26385  coseq00topi  26439  tanabsge  26443  logcnlem3  26581  atantan  26861  atanbnd  26864  cvxcl  26923  ostthlem1  27566  iscgrglt  28493  tgdim01ln  28543  lnxfr  28545  lnext  28546  tgfscgr  28547  tglineeltr  28610  colmid  28667  prodtp  32815  sgnmulsgn  32830  sgnmulsgp  32831  xrpxdivcld  32922  s3f1  32935  gsumtp  33045  cycpmco2  33109  cyc3co2  33116  archirngz  33165  archiabllem1b  33168  constrelextdg2  33781  constrfiss  33785  cos9thpiminplylem1  33816  esumcst  34097  hgt750lemb  34690  weiunso  36531  exp11d  42445  fnwe2lem3  43170  chner  47008