Theorem mpjaod 371

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

Syntax hints:   -> wi 4   \/ wo 358

This theorem is referenced by:  ecase2d  907  opth1  4394  reldmtpos  6446  dftpos4  6457  sorpssun  6488  sorpssin  6489  oaass  6763  nnawordex  6839  omabs  6849  suplub2  7422  cantnflt  7583  cantnfp1lem3  7592  en3lplem2  7627  tcrank  7764  cardaleph  7926  fpwwe2  8474  gchpwdom  8505  grur1  8651  indpi  8740  nn1suc  9977  nnsub  9994  seqid  11323  seqz  11326  faclbnd  11536  facavg  11547  bcval5  11564  hashnnn0genn0  11582  hashfzo  11649  sqrlem6  12008  resqrex  12011  absmod0  12063  absz  12071  iserex  12405  fsumf1o  12472  fsumss  12474  fsumcl2lem  12480  fsumadd  12487  fsummulc2  12522  fsumconst  12528  fsumrelem  12541  isumsplit  12575  absdvdsb  12823  dvdsabsb  12824  gcdabs1  12989  bezoutlem1  12993  bezoutlem2  12994  isprm5  13067  pcabs  13203  pockthg  13229  prmreclem5  13243  vdwlem13  13316  0ram  13343  ram0  13345  prmlem0  13383  mulgnn0ass  14874  mndodcongi  15136  oddvdsnn0  15137  odnncl  15138  efgredlemb  15333  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumconst  15487  gsumzmhm  15488  gsummulglem  15491  gsumzoppg  15494  pgpfac1lem5  15592  mplsubrglem  16457  gsumfsum  16721  zlpirlem1  16723  ordthaus  17402  icccmplem2  18807  metdstri  18834  ioombl  19412  itgabs  19679  dvlip  19830  dvge0  19843  dvivthlem1  19845  dvcnvrelem1  19854  ply1rem  20039  dgrcolem2  20145  quotcan  20179  sinq12ge0  20369  argregt0  20458  argrege0  20459  scvxcvx  20777  bpos1lem  21019  bposlem3  21023  lgseisenlem2  21087  gxneg  21807  gxsuc  21813  gxadd  21816  gxmul  21819  htthlem  22373  atcvati  23842  sinccvglem  25062  fprodf1o  25225  fprodss  25227  fprodcl2lem  25229  fprodmul  25237  fproddiv  25238  fprodconst  25255  fprodn0  25256  midofsegid  25942  outsideofeq  25968  hfun  26023  ordcmp  26101  itgabsnc  26173  pell1234qrdich  26814  psgnunilem2  27286  wallispilem3  27683  cvrat  29904  4atlem10  30088  4atlem12  30094  cdleme18d  30777  cdleme22b  30823  cdleme32e  30927  lclkrlem2e  31994

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-or 360