Theorem mpjaod 383

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

Syntax hints:   -> wi 4   \/ wo 370

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 189  df-or 372

This theorem is referenced by:  ecase2d  952  opth1  4678  sorpssun  6583  sorpssin  6584  reldmtpos  6986  dftpos4  6997  oaass  7267  nnawordex  7343  omabs  7353  suplub2  7980  en3lplem2  8125  cantnflt  8182  cantnfp1lem3  8190  tcrank  8360  cardaleph  8525  fpwwe2  9073  gchpwdom  9100  grur1  9250  indpi  9337  nn1suc  10637  nnsub  10655  seqid  12265  seqz  12268  faclbnd  12482  facavg  12493  bcval5  12510  hashnnn0genn0  12533  hashfzo  12608  sqrlem6  13323  resqrex  13326  absmod0  13378  absz  13386  iserex  13732  fsumf1o  13801  fsumss  13803  fsumcl2lem  13809  fsumadd  13817  fsummulc2  13857  fsumconst  13863  fsumrelem  13879  isumsplit  13910  fprodf1o  14012  fprodss  14014  fprodcl2lem  14016  fprodmul  14026  fproddiv  14027  fprodconst  14044  fprodn0  14045  absdvdsb  14333  dvdsabsb  14334  gcdabs1  14510  bezoutlem1  14515  bezoutlem2OLD  14516  bezoutlem2  14519  isprm5  14663  pcabs  14836  pockthg  14862  prmreclem5  14876  vdwlem13  14955  0ram  14990  ram0  14992  prmlem0  15089  mulgnn0ass  16799  psgnunilem2  17148  mndodcongi  17204  oddvdsnn0  17205  odnncl  17206  efgredlemb  17408  gsumzres  17555  gsumzcl2  17556  gsumzf1o  17558  gsumzaddlem  17566  gsumconst  17579  gsumzmhm  17582  gsummulglem  17586  gsumzoppg  17589  pgpfac1lem5  17724  mplsubrglem  18675  gsumfsum  19046  zringlpirlem1  19065  ordthaus  20412  icccmplem2  21853  metdstri  21880  metdstriOLD  21895  ioombl  22530  itgabs  22804  dvlip  22957  dvge0  22970  dvivthlem1  22972  dvcnvrelem1  22981  ply1rem  23126  dgrcolem2  23240  quotcan  23274  sinq12ge0  23475  argregt0  23571  argrege0  23572  scvxcvx  23923  bpos1lem  24222  bposlem3  24226  lgseisenlem2  24290  frgraregord013  25858  gxneg  26006  gxsuc  26012  gxadd  26015  gxmul  26018  htthlem  26582  atcvati  28051  sinccvglem  30328  midofsegid  30883  outsideofeq  30909  hfun  30957  ordcmp  31119  icoreclin  31772  itgabsnc  32023  dvasin  32040  cvrat  32999  4atlem10  33183  4atlem12  33189  cdleme18d  33873  cdleme22b  33920  cdleme32e  34024  lclkrlem2e  35091  pell1234qrdich  35719  suctrALT  37232  wallispilem3  37939  bgoldbtbnd  38914