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  924  opth1  4553  sorpssun  6356  sorpssin  6357  reldmtpos  6742  dftpos4  6753  oaass  6988  nnawordex  7064  omabs  7074  suplub2  7699  en3lplem2  7809  cantnflt  7868  cantnfp1lem3  7876  cantnfltOLD  7898  cantnfp1lem3OLD  7902  tcrank  8079  cardaleph  8247  fpwwe2  8798  gchpwdom  8825  grur1  8975  indpi  9064  nn1suc  10331  nnsub  10348  seqid  11835  seqz  11838  faclbnd  12050  facavg  12061  bcval5  12078  hashnnn0genn0  12098  hashfzo  12174  sqrlem6  12721  resqrex  12724  absmod0  12776  absz  12784  iserex  13118  fsumf1o  13184  fsumss  13186  fsumcl2lem  13192  fsumadd  13199  fsummulc2  13234  fsumconst  13240  fsumrelem  13253  isumsplit  13286  absdvdsb  13534  dvdsabsb  13535  gcdabs1  13701  bezoutlem1  13705  bezoutlem2  13706  isprm5  13781  pcabs  13924  pockthg  13950  prmreclem5  13964  vdwlem13  14037  0ram  14064  ram0  14066  prmlem0  14116  mulgnn0ass  15636  psgnunilem2  15981  mndodcongi  16026  oddvdsnn0  16027  odnncl  16028  efgredlemb  16223  gsumzres  16368  gsumzcl2  16369  gsumzf1o  16371  gsumzresOLD  16372  gsumzclOLD  16373  gsumzf1oOLD  16374  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsumconst  16406  gsumzmhm  16407  gsumzmhmOLD  16408  gsummulglem  16413  gsumzoppg  16416  gsumzoppgOLD  16417  pgpfac1lem5  16554  mplsubrglem  17451  mplsubrglemOLD  17452  gsumfsum  17723  zringlpirlem1  17745  zlpirlem1  17750  ordthaus  18830  icccmplem2  20242  metdstri  20269  ioombl  20888  itgabs  21154  dvlip  21307  dvge0  21320  dvivthlem1  21322  dvcnvrelem1  21331  ply1rem  21520  dgrcolem2  21626  quotcan  21660  sinq12ge0  21855  argregt0  21944  argrege0  21945  scvxcvx  22264  bpos1lem  22506  bposlem3  22510  lgseisenlem2  22574  gxneg  23576  gxsuc  23582  gxadd  23585  gxmul  23588  htthlem  24142  atcvati  25613  sinccvglem  27164  fprodf1o  27306  fprodss  27308  fprodcl2lem  27310  fprodmul  27318  fproddiv  27319  fprodconst  27336  fprodn0  27337  midofsegid  27982  outsideofeq  28008  hfun  28063  ordcmp  28141  itgabsnc  28305  dvasin  28324  pell1234qrdich  29047  wallispilem3  29708  frgraregord013  30557  suctrALT  31264  cvrat  32639  4atlem10  32823  4atlem12  32829  cdleme18d  33512  cdleme22b  33558  cdleme32e  33662  lclkrlem2e  34729