Theorem mpjaod 381

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

Step	Hyp	Ref	Expression
1		jaod.3	. 2 |- ( ph -> ( ps \/ th ) )
2		jaod.1	. . 3 |- ( ph -> ( ps -> ch ) )
3		jaod.2	. . 3 |- ( ph -> ( th -> ch ) )
4	2, 3	jaod 380	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
5	1, 4	mpd 15	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   \/ wo 368

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

This theorem is referenced by:  ecase2d  931  opth1  4560  sorpssun  6362  sorpssin  6363  reldmtpos  6748  dftpos4  6759  oaass  6992  nnawordex  7068  omabs  7078  suplub2  7703  en3lplem2  7813  cantnflt  7872  cantnfp1lem3  7880  cantnfltOLD  7902  cantnfp1lem3OLD  7906  tcrank  8083  cardaleph  8251  fpwwe2  8802  gchpwdom  8829  grur1  8979  indpi  9068  nn1suc  10335  nnsub  10352  seqid  11843  seqz  11846  faclbnd  12058  facavg  12069  bcval5  12086  hashnnn0genn0  12106  hashfzo  12182  sqrlem6  12729  resqrex  12732  absmod0  12784  absz  12792  iserex  13126  fsumf1o  13192  fsumss  13194  fsumcl2lem  13200  fsumadd  13207  fsummulc2  13243  fsumconst  13249  fsumrelem  13262  isumsplit  13295  absdvdsb  13543  dvdsabsb  13544  gcdabs1  13710  bezoutlem1  13714  bezoutlem2  13715  isprm5  13790  pcabs  13933  pockthg  13959  prmreclem5  13973  vdwlem13  14046  0ram  14073  ram0  14075  prmlem0  14125  mulgnn0ass  15647  psgnunilem2  15992  mndodcongi  16037  oddvdsnn0  16038  odnncl  16039  efgredlemb  16234  gsumzres  16379  gsumzcl2  16380  gsumzf1o  16382  gsumzresOLD  16383  gsumzclOLD  16384  gsumzf1oOLD  16385  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsumconst  16417  gsumzmhm  16420  gsumzmhmOLD  16421  gsummulglem  16427  gsumzoppg  16430  gsumzoppgOLD  16431  pgpfac1lem5  16568  mplsubrglem  17494  mplsubrglemOLD  17495  gsumfsum  17854  zringlpirlem1  17878  zlpirlem1  17883  ordthaus  18963  icccmplem2  20375  metdstri  20402  ioombl  21021  itgabs  21287  dvlip  21440  dvge0  21453  dvivthlem1  21455  dvcnvrelem1  21464  ply1rem  21610  dgrcolem2  21716  quotcan  21750  sinq12ge0  21945  argregt0  22034  argrege0  22035  scvxcvx  22354  bpos1lem  22596  bposlem3  22600  lgseisenlem2  22664  gxneg  23704  gxsuc  23710  gxadd  23713  gxmul  23716  htthlem  24270  atcvati  25741  sinccvglem  27268  fprodf1o  27410  fprodss  27412  fprodcl2lem  27414  fprodmul  27422  fproddiv  27423  fprodconst  27440  fprodn0  27441  midofsegid  28086  outsideofeq  28112  hfun  28167  ordcmp  28245  itgabsnc  28414  dvasin  28433  pell1234qrdich  29155  wallispilem3  29815  frgraregord013  30664  suctrALT  31449  cvrat  32906  4atlem10  33090  4atlem12  33096  cdleme18d  33779  cdleme22b  33825  cdleme32e  33929  lclkrlem2e  34996