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  938  opth1  4720  sorpssun  6570  sorpssin  6571  reldmtpos  6963  dftpos4  6974  oaass  7210  nnawordex  7286  omabs  7296  suplub2  7920  en3lplem2  8031  cantnflt  8090  cantnfp1lem3  8098  cantnfltOLD  8120  cantnfp1lem3OLD  8124  tcrank  8301  cardaleph  8469  fpwwe2  9020  gchpwdom  9047  grur1  9197  indpi  9284  nn1suc  10556  nnsub  10573  seqid  12119  seqz  12122  faclbnd  12335  facavg  12346  bcval5  12363  hashnnn0genn0  12383  hashfzo  12451  sqrlem6  13043  resqrex  13046  absmod0  13098  absz  13106  iserex  13441  fsumf1o  13507  fsumss  13509  fsumcl2lem  13515  fsumadd  13523  fsummulc2  13561  fsumconst  13567  fsumrelem  13583  isumsplit  13614  absdvdsb  13862  dvdsabsb  13863  gcdabs1  14030  bezoutlem1  14034  bezoutlem2  14035  isprm5  14111  pcabs  14256  pockthg  14282  prmreclem5  14296  vdwlem13  14369  0ram  14396  ram0  14398  prmlem0  14448  mulgnn0ass  15978  psgnunilem2  16323  mndodcongi  16370  oddvdsnn0  16371  odnncl  16372  efgredlemb  16567  gsumzres  16714  gsumzcl2  16715  gsumzf1o  16717  gsumzresOLD  16718  gsumzclOLD  16719  gsumzf1oOLD  16720  gsumzaddlem  16734  gsumzaddlemOLD  16736  gsumconst  16754  gsumzmhm  16757  gsumzmhmOLD  16758  gsummulglem  16764  gsumzoppg  16767  gsumzoppgOLD  16768  pgpfac1lem5  16929  mplsubrglem  17887  mplsubrglemOLD  17888  gsumfsum  18268  zringlpirlem1  18292  zlpirlem1  18297  ordthaus  19667  icccmplem2  21079  metdstri  21106  ioombl  21726  itgabs  21992  dvlip  22145  dvge0  22158  dvivthlem1  22160  dvcnvrelem1  22169  ply1rem  22315  dgrcolem2  22421  quotcan  22455  sinq12ge0  22650  argregt0  22739  argrege0  22740  scvxcvx  23059  bpos1lem  23301  bposlem3  23305  lgseisenlem2  23369  frgraregord013  24811  gxneg  24960  gxsuc  24966  gxadd  24969  gxmul  24972  htthlem  25526  atcvati  26997  sinccvglem  28529  fprodf1o  28671  fprodss  28673  fprodcl2lem  28675  fprodmul  28683  fproddiv  28684  fprodconst  28701  fprodn0  28702  midofsegid  29347  outsideofeq  29373  hfun  29428  ordcmp  29505  itgabsnc  29677  dvasin  29696  pell1234qrdich  30417  wallispilem3  31383  suctrALT  32715  cvrat  34227  4atlem10  34411  4atlem12  34417  cdleme18d  35100  cdleme22b  35146  cdleme32e  35250  lclkrlem2e  36317