Theorem mpjaod 396

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

Syntax hints:   -> wi 4   \/ wo 383

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 197  df-or 385

This theorem is referenced by:  ecase2d  981  opth1  4944  sorpssun  6944  sorpssin  6945  reldmtpos  7360  dftpos4  7371  oaass  7641  nnawordex  7717  omabs  7727  suplub2  8367  en3lplem2  8512  cantnflt  8569  cantnfp1lem3  8577  tcrank  8747  cardaleph  8912  fpwwe2  9465  gchpwdom  9492  grur1  9642  indpi  9729  nn1suc  11041  nnsub  11059  seqid  12846  seqz  12849  faclbnd  13077  facavg  13088  bcval5  13105  hashnnn0genn0  13131  hashfzo  13216  sqrlem6  13988  resqrex  13991  absmod0  14043  absz  14051  iserex  14387  fsumf1o  14454  fsumss  14456  fsumcl2lem  14462  fsumadd  14470  fsummulc2  14516  fsumconst  14522  fsumrelem  14539  isumsplit  14572  fprodf1o  14676  fprodss  14678  fprodcl2lem  14680  fprodmul  14690  fproddiv  14691  fprodconst  14708  fprodn0  14709  absdvdsb  15000  dvdsabsb  15001  gcdabs1  15251  bezoutlem1  15256  bezoutlem2  15257  isprm5  15419  pcabs  15579  pockthg  15610  prmreclem5  15624  vdwlem13  15697  0ram  15724  ram0  15726  prmlem0  15812  mulgnn0ass  17578  psgnunilem2  17915  mndodcongi  17962  oddvdsnn0  17963  odnncl  17964  efgredlemb  18159  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  gsummulglem  18341  gsumzoppg  18344  pgpfac1lem5  18478  mplsubrglem  19439  gsumfsum  19813  zringlpirlem1  19832  ordthaus  21188  icccmplem2  22626  metdstri  22654  ioombl  23333  itgabs  23601  dvlip  23756  dvge0  23769  dvivthlem1  23771  dvcnvrelem1  23780  ply1rem  23923  dgrcolem2  24030  quotcan  24064  sinq12ge0  24260  argregt0  24356  argrege0  24357  scvxcvx  24712  bpos1lem  25007  bposlem3  25011  lgseisenlem2  25101  frgrregord013  27253  htthlem  27774  atcvati  29245  sinccvglem  31566  noextendseq  31820  noetalem3  31865  midofsegid  32211  outsideofeq  32237  hfun  32285  ordcmp  32446  icoreclin  33205  itgabsnc  33479  dvasin  33496  cvrat  34708  4atlem10  34892  4atlem12  34898  cdleme18d  35582  cdleme22b  35629  cdleme32e  35733  lclkrlem2e  36800  pell1234qrdich  37425  clsk1indlem3  38341  suctrALT  39061  wallispilem3  40284  bgoldbtbnd  41697