MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpjao3dan Structured version   Visualization version   GIF version

Theorem mpjao3dan 1433
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
StepHypRef Expression
1 mpjao3dan.4 . 2 (𝜑 → (𝜓𝜃𝜏))
2 mpjao3dan.1 . . 3 ((𝜑𝜓) → 𝜒)
3 mpjao3dan.2 . . 3 ((𝜑𝜃) → 𝜒)
4 mpjao3dan.3 . . 3 ((𝜑𝜏) → 𝜒)
52, 3, 43jaodan 1432 . 2 ((𝜑 ∧ (𝜓𝜃𝜏)) → 𝜒)
61, 5mpdan 687 1 (𝜑𝜒)
Colors of variables: wff setvar class
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  9588  r1val1  9827  xleadd1a  13296  xlt2add  13303  xmullem  13307  xmulgt0  13326  xmulasslem3  13329  xlemul1a  13331  xadddilem  13337  xadddi  13338  xadddi2  13340  isxmet2d  24338  icccvx  24982  ivthicc  25494  mbfmulc2lem  25683  c1lip1  26037  dvivth  26050  reeff1o  26492  coseq00topi  26545  tanabsge  26549  logcnlem3  26687  atantan  26967  atanbnd  26970  cvxcl  27029  ostthlem1  27672  iscgrglt  28523  tgdim01ln  28573  lnxfr  28575  lnext  28576  tgfscgr  28577  tglineeltr  28640  colmid  28697  prodtp  32830  xrpxdivcld  32918  s3f1  32932  gsumtp  33062  cycpmco2  33154  cyc3co2  33161  archirngz  33197  archiabllem1b  33200  constrelextdg2  33789  esumcst  34065  sgnmulsgn  34553  sgnmulsgp  34554  hgt750lemb  34672  weiunso  36468  exp11d  42366  fnwe2lem3  43069
  Copyright terms: Public domain W3C validator