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 686 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ 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 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086 This theorem is referenced by:  wemaplem2  9008  r1val1  9212  xleadd1a  12643  xlt2add  12650  xmullem  12654  xmulgt0  12673  xmulasslem3  12676  xlemul1a  12678  xadddilem  12684  xadddi  12685  xadddi2  12687  isxmet2d  22937  icccvx  23558  ivthicc  24065  mbfmulc2lem  24254  c1lip1  24603  dvivth  24616  reeff1o  25045  coseq00topi  25098  tanabsge  25102  logcnlem3  25238  atantan  25512  atanbnd  25515  cvxcl  25573  ostthlem1  26214  iscgrglt  26311  tgdim01ln  26361  lnxfr  26363  lnext  26364  tgfscgr  26365  tglineeltr  26428  colmid  26485  prodtp  30554  xrpxdivcld  30622  s3f1  30634  cycpmco2  30807  cyc3co2  30814  archirngz  30850  archiabllem1b  30853  esumcst  31379  sgnmulsgn  31864  sgnmulsgp  31865  hgt750lemb  31984  fnwe2lem3  39912
 Copyright terms: Public domain W3C validator