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

Theorem mpjao3dan 1295
Description: Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.)
Hypotheses
Ref Expression
mpjao3dan.1
mpjao3dan.2
mpjao3dan.3
mpjao3dan.4
Assertion
Ref Expression
mpjao3dan

Proof of Theorem mpjao3dan
StepHypRef Expression
1 mpjao3dan.1 . . 3
2 mpjao3dan.2 . . 3
31, 2jaodan 785 . 2
4 mpjao3dan.3 . 2
5 mpjao3dan.4 . . 3
6 df-3or 974 . . 3
75, 6sylib 196 . 2
83, 4, 7mpjaodan 786 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368  /\wa 369  \/w3o 972
This theorem is referenced by:  wemaplem2  7993  r1val1  8225  xleadd1a  11474  xlt2add  11481  xmullem  11485  xmulgt0  11504  xmulasslem3  11507  xlemul1a  11509  xadddilem  11515  xadddi  11516  xadddi2  11518  isxmet2d  20830  icccvx  21450  ivthicc  21870  mbfmulc2lem  22054  c1lip1  22398  dvivth  22411  reeff1o  22842  coseq00topi  22895  tanabsge  22899  logcnlem3  23025  atantan  23254  atanbnd  23257  cvxcl  23314  ostthlem1  23812  tgdim01ln  23951  lnxfr  23953  lnext  23954  tgfscgr  23955  tglineeltr  24011  colmid  24065  xrpxdivcld  27631  archirngz  27733  archiabllem1b  27736  esumcst  28071  sgnmulsgn  28488  sgnmulsgp  28489  fnwe2lem3  30998
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 185  df-or 370  df-an 371  df-3or 974
  Copyright terms: Public domain W3C validator