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

Theorem mpjaod 371
Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)
Hypotheses
Ref Expression
jaod.1  |-  ( ph  ->  ( ps  ->  ch ) )
jaod.2  |-  ( ph  ->  ( th  ->  ch ) )
jaod.3  |-  ( ph  ->  ( ps  \/  th ) )
Assertion
Ref Expression
mpjaod  |-  ( ph  ->  ch )

Proof of Theorem mpjaod
StepHypRef Expression
1 jaod.3 . 2  |-  ( ph  ->  ( ps  \/  th ) )
2 jaod.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 jaod.2 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
42, 3jaod 370 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
51, 4mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358
This theorem is referenced by:  ecase2d  907  opth1  4426  suctr  4657  reldmtpos  6479  dftpos4  6490  sorpssun  6521  sorpssin  6522  oaass  6796  nnawordex  6872  omabs  6882  suplub2  7458  cantnflt  7619  cantnfp1lem3  7628  en3lplem2  7663  tcrank  7800  cardaleph  7962  fpwwe2  8510  gchpwdom  8541  grur1  8687  indpi  8776  nn1suc  10013  nnsub  10030  seqid  11360  seqz  11363  faclbnd  11573  facavg  11584  bcval5  11601  hashnnn0genn0  11619  hashfzo  11686  sqrlem6  12045  resqrex  12048  absmod0  12100  absz  12108  iserex  12442  fsumf1o  12509  fsumss  12511  fsumcl2lem  12517  fsumadd  12524  fsummulc2  12559  fsumconst  12565  fsumrelem  12578  isumsplit  12612  absdvdsb  12860  dvdsabsb  12861  gcdabs1  13026  bezoutlem1  13030  bezoutlem2  13031  isprm5  13104  pcabs  13240  pockthg  13266  prmreclem5  13280  vdwlem13  13353  0ram  13380  ram0  13382  prmlem0  13420  mulgnn0ass  14911  mndodcongi  15173  oddvdsnn0  15174  odnncl  15175  efgredlemb  15370  gsumzres  15509  gsumzcl  15510  gsumzf1o  15511  gsumzaddlem  15518  gsumconst  15524  gsumzmhm  15525  gsummulglem  15528  gsumzoppg  15531  pgpfac1lem5  15629  mplsubrglem  16494  gsumfsum  16758  zlpirlem1  16760  ordthaus  17440  icccmplem2  18846  metdstri  18873  ioombl  19451  itgabs  19718  dvlip  19869  dvge0  19882  dvivthlem1  19884  dvcnvrelem1  19893  ply1rem  20078  dgrcolem2  20184  quotcan  20218  sinq12ge0  20408  argregt0  20497  argrege0  20498  scvxcvx  20816  bpos1lem  21058  bposlem3  21062  lgseisenlem2  21126  gxneg  21846  gxsuc  21852  gxadd  21855  gxmul  21858  htthlem  22412  atcvati  23881  sinccvglem  25101  fprodf1o  25264  fprodss  25266  fprodcl2lem  25268  fprodmul  25276  fproddiv  25277  fprodconst  25294  fprodn0  25295  midofsegid  26030  outsideofeq  26056  hfun  26111  ordcmp  26189  itgabsnc  26264  pell1234qrdich  26915  psgnunilem2  27386  wallispilem3  27783  cvrat  30156  4atlem10  30340  4atlem12  30346  cdleme18d  31029  cdleme22b  31075  cdleme32e  31179  lclkrlem2e  32246
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator