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

Theorem mpjao3dan 1428
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 1427 . 2 ((𝜑 ∧ (𝜓𝜃𝜏)) → 𝜒)
61, 5mpdan 685 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3o 1083
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 395  df-or 846  df-3or 1085  df-3an 1086
This theorem is referenced by:  wemaplem2  9572  r1val1  9811  xleadd1a  13267  xlt2add  13274  xmullem  13278  xmulgt0  13297  xmulasslem3  13300  xlemul1a  13302  xadddilem  13308  xadddi  13309  xadddi2  13311  isxmet2d  24277  icccvx  24919  ivthicc  25431  mbfmulc2lem  25620  c1lip1  25974  dvivth  25987  reeff1o  26429  coseq00topi  26482  tanabsge  26486  logcnlem3  26623  atantan  26900  atanbnd  26903  cvxcl  26962  ostthlem1  27605  iscgrglt  28390  tgdim01ln  28440  lnxfr  28442  lnext  28443  tgfscgr  28444  tglineeltr  28507  colmid  28564  prodtp  32675  xrpxdivcld  32743  s3f1  32757  cycpmco2  32946  cyc3co2  32953  archirngz  32989  archiabllem1b  32992  esumcst  33810  sgnmulsgn  34297  sgnmulsgp  34298  hgt750lemb  34416  exp11d  42017  fnwe2lem3  42615
  Copyright terms: Public domain W3C validator