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  931  opth1  4676  sorpssun  6480  sorpssin  6481  reldmtpos  6866  dftpos4  6877  oaass  7113  nnawordex  7189  omabs  7199  suplub2  7825  en3lplem2  7935  cantnflt  7994  cantnfp1lem3  8002  cantnfltOLD  8024  cantnfp1lem3OLD  8028  tcrank  8205  cardaleph  8373  fpwwe2  8924  gchpwdom  8951  grur1  9101  indpi  9190  nn1suc  10457  nnsub  10474  seqid  11971  seqz  11974  faclbnd  12186  facavg  12197  bcval5  12214  hashnnn0genn0  12234  hashfzo  12311  sqrlem6  12858  resqrex  12861  absmod0  12913  absz  12921  iserex  13255  fsumf1o  13321  fsumss  13323  fsumcl2lem  13329  fsumadd  13336  fsummulc2  13372  fsumconst  13378  fsumrelem  13391  isumsplit  13424  absdvdsb  13672  dvdsabsb  13673  gcdabs1  13839  bezoutlem1  13843  bezoutlem2  13844  isprm5  13919  pcabs  14062  pockthg  14088  prmreclem5  14102  vdwlem13  14175  0ram  14202  ram0  14204  prmlem0  14254  mulgnn0ass  15778  psgnunilem2  16123  mndodcongi  16170  oddvdsnn0  16171  odnncl  16172  efgredlemb  16367  gsumzres  16512  gsumzcl2  16513  gsumzf1o  16515  gsumzresOLD  16516  gsumzclOLD  16517  gsumzf1oOLD  16518  gsumzaddlem  16532  gsumzaddlemOLD  16534  gsumconst  16552  gsumzmhm  16555  gsumzmhmOLD  16556  gsummulglem  16562  gsumzoppg  16565  gsumzoppgOLD  16566  pgpfac1lem5  16705  mplsubrglem  17644  mplsubrglemOLD  17645  gsumfsum  18007  zringlpirlem1  18031  zlpirlem1  18036  ordthaus  19123  icccmplem2  20535  metdstri  20562  ioombl  21182  itgabs  21448  dvlip  21601  dvge0  21614  dvivthlem1  21616  dvcnvrelem1  21625  ply1rem  21771  dgrcolem2  21877  quotcan  21911  sinq12ge0  22106  argregt0  22195  argrege0  22196  scvxcvx  22515  bpos1lem  22757  bposlem3  22761  lgseisenlem2  22825  gxneg  23925  gxsuc  23931  gxadd  23934  gxmul  23937  htthlem  24491  atcvati  25962  sinccvglem  27481  fprodf1o  27623  fprodss  27625  fprodcl2lem  27627  fprodmul  27635  fproddiv  27636  fprodconst  27653  fprodn0  27654  midofsegid  28299  outsideofeq  28325  hfun  28380  ordcmp  28457  itgabsnc  28629  dvasin  28648  pell1234qrdich  29370  wallispilem3  30030  frgraregord013  30879  suctrALT  31914  cvrat  33424  4atlem10  33608  4atlem12  33614  cdleme18d  34297  cdleme22b  34343  cdleme32e  34447  lclkrlem2e  35514