Theorem mpjaod 379

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 378	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
5	1, 4	mpd 15	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   \/ wo 366

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 368

This theorem is referenced by:  ecase2d  941  opth1  4663  sorpssun  6568  sorpssin  6569  reldmtpos  6965  dftpos4  6976  oaass  7246  nnawordex  7322  omabs  7332  suplub2  7953  en3lplem2  8064  cantnflt  8122  cantnfp1lem3  8130  cantnfltOLD  8152  cantnfp1lem3OLD  8156  tcrank  8333  cardaleph  8501  fpwwe2  9050  gchpwdom  9077  grur1  9227  indpi  9314  nn1suc  10596  nnsub  10614  seqid  12194  seqz  12197  faclbnd  12410  facavg  12421  bcval5  12438  hashnnn0genn0  12461  hashfzo  12534  sqrlem6  13228  resqrex  13231  absmod0  13283  absz  13291  iserex  13626  fsumf1o  13692  fsumss  13694  fsumcl2lem  13700  fsumadd  13708  fsummulc2  13748  fsumconst  13754  fsumrelem  13770  isumsplit  13801  fprodf1o  13903  fprodss  13905  fprodcl2lem  13907  fprodmul  13915  fproddiv  13916  fprodconst  13932  fprodn0  13933  absdvdsb  14209  dvdsabsb  14210  gcdabs1  14379  bezoutlem1  14383  bezoutlem2  14384  isprm5  14460  pcabs  14605  pockthg  14631  prmreclem5  14645  vdwlem13  14718  0ram  14745  ram0  14747  prmlem0  14798  mulgnn0ass  16493  psgnunilem2  16842  mndodcongi  16889  oddvdsnn0  16890  odnncl  16891  efgredlemb  17086  gsumzres  17236  gsumzcl2  17237  gsumzf1o  17239  gsumzresOLD  17240  gsumzclOLD  17241  gsumzf1oOLD  17242  gsumzaddlem  17256  gsumzaddlemOLD  17258  gsumconst  17275  gsumzmhm  17278  gsumzmhmOLD  17279  gsummulglem  17285  gsumzoppg  17288  gsumzoppgOLD  17289  pgpfac1lem5  17448  mplsubrglem  18418  mplsubrglemOLD  18419  gsumfsum  18802  zringlpirlem1  18820  ordthaus  20176  icccmplem2  21618  metdstri  21645  ioombl  22265  itgabs  22531  dvlip  22684  dvge0  22697  dvivthlem1  22699  dvcnvrelem1  22708  ply1rem  22854  dgrcolem2  22961  quotcan  22995  sinq12ge0  23191  argregt0  23287  argrege0  23288  scvxcvx  23639  bpos1lem  23936  bposlem3  23940  lgseisenlem2  24004  frgraregord013  25522  gxneg  25668  gxsuc  25674  gxadd  25677  gxmul  25680  htthlem  26234  atcvati  27704  sinccvglem  29877  midofsegid  30429  outsideofeq  30455  hfun  30503  ordcmp  30666  icoreclin  31261  itgabsnc  31437  dvasin  31454  cvrat  32419  4atlem10  32603  4atlem12  32609  cdleme18d  33293  cdleme22b  33340  cdleme32e  33444  lclkrlem2e  34511  pell1234qrdich  35138  suctrALT  36636  wallispilem3  37198  bgoldbtbnd  37838