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

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
StepHypRef Expression
1 mpjao3dan.4 . 2 (𝜑 → (𝜓𝜃𝜏))
2 mpjao3dan.1 . . 3 ((𝜑𝜓) → 𝜒)
3 mpjao3dan.2 . . 3 ((𝜑𝜃) → 𝜒)
4 mpjao3dan.3 . . 3 ((𝜑𝜏) → 𝜒)
52, 3, 43jaodan 1431 . 2 ((𝜑 ∧ (𝜓𝜃𝜏)) → 𝜒)
61, 5mpdan 686 1 (𝜑𝜒)
Colors of variables: wff setvar class
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  9491  r1val1  9730  xleadd1a  13181  xlt2add  13188  xmullem  13192  xmulgt0  13211  xmulasslem3  13214  xlemul1a  13216  xadddilem  13222  xadddi  13223  xadddi2  13225  isxmet2d  23703  icccvx  24336  ivthicc  24845  mbfmulc2lem  25034  c1lip1  25384  dvivth  25397  reeff1o  25829  coseq00topi  25882  tanabsge  25886  logcnlem3  26022  atantan  26296  atanbnd  26299  cvxcl  26357  ostthlem1  26998  iscgrglt  27505  tgdim01ln  27555  lnxfr  27557  lnext  27558  tgfscgr  27559  tglineeltr  27622  colmid  27679  prodtp  31779  xrpxdivcld  31847  s3f1  31859  cycpmco2  32038  cyc3co2  32045  archirngz  32081  archiabllem1b  32084  esumcst  32726  sgnmulsgn  33213  sgnmulsgp  33214  hgt750lemb  33333  exp11d  40858  fnwe2lem3  41426
  Copyright terms: Public domain W3C validator