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

Theorem mpjaod 381
Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)
Hypotheses
Ref Expression
jaod.1
jaod.2
jaod.3
Assertion
Ref Expression
mpjaod

Proof of Theorem mpjaod
StepHypRef Expression
1 jaod.3 . 2
2 jaod.1 . . 3
3 jaod.2 . . 3
42, 3jaod 380 . 2
51, 4mpd 15 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368
This theorem is referenced by:  ecase2d  940  opth1  4725  sorpssun  6587  sorpssin  6588  reldmtpos  6982  dftpos4  6993  oaass  7229  nnawordex  7305  omabs  7315  suplub2  7941  en3lplem2  8053  cantnflt  8112  cantnfp1lem3  8120  cantnfltOLD  8142  cantnfp1lem3OLD  8146  tcrank  8323  cardaleph  8491  fpwwe2  9042  gchpwdom  9069  grur1  9219  indpi  9306  nn1suc  10582  nnsub  10599  seqid  12152  seqz  12155  faclbnd  12368  facavg  12379  bcval5  12396  hashnnn0genn0  12416  hashfzo  12487  sqrlem6  13081  resqrex  13084  absmod0  13136  absz  13144  iserex  13479  fsumf1o  13545  fsumss  13547  fsumcl2lem  13553  fsumadd  13561  fsummulc2  13599  fsumconst  13605  fsumrelem  13621  isumsplit  13652  fprodf1o  13753  fprodss  13755  fprodcl2lem  13757  fprodmul  13765  fproddiv  13766  fprodconst  13782  fprodn0  13783  absdvdsb  14002  dvdsabsb  14003  gcdabs1  14172  bezoutlem1  14176  bezoutlem2  14177  isprm5  14253  pcabs  14398  pockthg  14424  prmreclem5  14438  vdwlem13  14511  0ram  14538  ram0  14540  prmlem0  14591  mulgnn0ass  16171  psgnunilem2  16520  mndodcongi  16567  oddvdsnn0  16568  odnncl  16569  efgredlemb  16764  gsumzres  16914  gsumzcl2  16915  gsumzf1o  16917  gsumzresOLD  16918  gsumzclOLD  16919  gsumzf1oOLD  16920  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumconst  16954  gsumzmhm  16957  gsumzmhmOLD  16958  gsummulglem  16964  gsumzoppg  16967  gsumzoppgOLD  16968  pgpfac1lem5  17130  mplsubrglem  18100  mplsubrglemOLD  18101  gsumfsum  18484  zringlpirlem1  18509  zlpirlem1  18514  ordthaus  19885  icccmplem2  21328  metdstri  21355  ioombl  21975  itgabs  22241  dvlip  22394  dvge0  22407  dvivthlem1  22409  dvcnvrelem1  22418  ply1rem  22564  dgrcolem2  22671  quotcan  22705  sinq12ge0  22901  argregt0  22995  argrege0  22996  scvxcvx  23315  bpos1lem  23557  bposlem3  23561  lgseisenlem2  23625  frgraregord013  25118  gxneg  25268  gxsuc  25274  gxadd  25277  gxmul  25280  htthlem  25834  atcvati  27305  sinccvglem  29038  midofsegid  29754  outsideofeq  29780  hfun  29835  ordcmp  29912  itgabsnc  30084  dvasin  30103  pell1234qrdich  30797  wallispilem3  31849  suctrALT  33626  cvrat  35146  4atlem10  35330  4atlem12  35336  cdleme18d  36020  cdleme22b  36067  cdleme32e  36171  lclkrlem2e  37238
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
  Copyright terms: Public domain W3C validator