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  940  opth1  4710  sorpssun  6572  sorpssin  6573  reldmtpos  6965  dftpos4  6976  oaass  7212  nnawordex  7288  omabs  7298  suplub2  7923  en3lplem2  8035  cantnflt  8094  cantnfp1lem3  8102  cantnfltOLD  8124  cantnfp1lem3OLD  8128  tcrank  8305  cardaleph  8473  fpwwe2  9024  gchpwdom  9051  grur1  9201  indpi  9288  nn1suc  10564  nnsub  10581  seqid  12134  seqz  12137  faclbnd  12350  facavg  12361  bcval5  12378  hashnnn0genn0  12398  hashfzo  12469  sqrlem6  13063  resqrex  13066  absmod0  13118  absz  13126  iserex  13461  fsumf1o  13527  fsumss  13529  fsumcl2lem  13535  fsumadd  13543  fsummulc2  13581  fsumconst  13587  fsumrelem  13603  isumsplit  13634  fprodf1o  13735  fprodss  13737  fprodcl2lem  13739  fprodmul  13747  fproddiv  13748  fprodconst  13764  fprodn0  13765  absdvdsb  13984  dvdsabsb  13985  gcdabs1  14154  bezoutlem1  14158  bezoutlem2  14159  isprm5  14235  pcabs  14380  pockthg  14406  prmreclem5  14420  vdwlem13  14493  0ram  14520  ram0  14522  prmlem0  14573  mulgnn0ass  16150  psgnunilem2  16499  mndodcongi  16546  oddvdsnn0  16547  odnncl  16548  efgredlemb  16743  gsumzres  16893  gsumzcl2  16894  gsumzf1o  16896  gsumzresOLD  16897  gsumzclOLD  16898  gsumzf1oOLD  16899  gsumzaddlem  16913  gsumzaddlemOLD  16915  gsumconst  16933  gsumzmhm  16936  gsumzmhmOLD  16937  gsummulglem  16943  gsumzoppg  16946  gsumzoppgOLD  16947  pgpfac1lem5  17109  mplsubrglem  18079  mplsubrglemOLD  18080  gsumfsum  18463  zringlpirlem1  18487  zlpirlem1  18492  ordthaus  19863  icccmplem2  21306  metdstri  21333  ioombl  21953  itgabs  22219  dvlip  22372  dvge0  22385  dvivthlem1  22387  dvcnvrelem1  22396  ply1rem  22542  dgrcolem2  22649  quotcan  22683  sinq12ge0  22879  argregt0  22973  argrege0  22974  scvxcvx  23293  bpos1lem  23535  bposlem3  23539  lgseisenlem2  23603  frgraregord013  25096  gxneg  25246  gxsuc  25252  gxadd  25255  gxmul  25258  htthlem  25812  atcvati  27283  sinccvglem  29016  midofsegid  29730  outsideofeq  29756  hfun  29811  ordcmp  29888  itgabsnc  30060  dvasin  30079  pell1234qrdich  30773  wallispilem3  31803  suctrALT  33494  cvrat  35021  4atlem10  35205  4atlem12  35211  cdleme18d  35895  cdleme22b  35942  cdleme32e  36046  lclkrlem2e  37113