Theorem mpjaod 382

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

Syntax hints:   -> wi 4   \/ wo 369

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 188  df-or 371

This theorem is referenced by:  ecase2d  948  opth1  4691  sorpssun  6589  sorpssin  6590  reldmtpos  6986  dftpos4  6997  oaass  7267  nnawordex  7343  omabs  7353  suplub2  7978  en3lplem2  8123  cantnflt  8179  cantnfp1lem3  8187  tcrank  8357  cardaleph  8521  fpwwe2  9069  gchpwdom  9096  grur1  9246  indpi  9333  nn1suc  10631  nnsub  10649  seqid  12258  seqz  12261  faclbnd  12475  facavg  12486  bcval5  12503  hashnnn0genn0  12526  hashfzo  12599  sqrlem6  13300  resqrex  13303  absmod0  13355  absz  13363  iserex  13708  fsumf1o  13777  fsumss  13779  fsumcl2lem  13785  fsumadd  13793  fsummulc2  13833  fsumconst  13839  fsumrelem  13855  isumsplit  13886  fprodf1o  13988  fprodss  13990  fprodcl2lem  13992  fprodmul  14002  fproddiv  14003  fprodconst  14020  fprodn0  14021  absdvdsb  14309  dvdsabsb  14310  gcdabs1  14486  bezoutlem1  14491  bezoutlem2OLD  14492  bezoutlem2  14495  isprm5  14639  pcabs  14812  pockthg  14838  prmreclem5  14852  vdwlem13  14931  0ram  14966  ram0  14968  prmlem0  15065  mulgnn0ass  16775  psgnunilem2  17124  mndodcongi  17180  oddvdsnn0  17181  odnncl  17182  efgredlemb  17384  gsumzres  17531  gsumzcl2  17532  gsumzf1o  17534  gsumzaddlem  17542  gsumconst  17555  gsumzmhm  17558  gsummulglem  17562  gsumzoppg  17565  pgpfac1lem5  17700  mplsubrglem  18651  gsumfsum  19022  zringlpirlem1  19040  ordthaus  20387  icccmplem2  21828  metdstri  21855  metdstriOLD  21870  ioombl  22505  itgabs  22779  dvlip  22932  dvge0  22945  dvivthlem1  22947  dvcnvrelem1  22956  ply1rem  23101  dgrcolem2  23215  quotcan  23249  sinq12ge0  23450  argregt0  23546  argrege0  23547  scvxcvx  23898  bpos1lem  24197  bposlem3  24201  lgseisenlem2  24265  frgraregord013  25832  gxneg  25980  gxsuc  25986  gxadd  25989  gxmul  25992  htthlem  26556  atcvati  28025  sinccvglem  30312  midofsegid  30864  outsideofeq  30890  hfun  30938  ordcmp  31100  icoreclin  31701  itgabsnc  31925  dvasin  31942  cvrat  32906  4atlem10  33090  4atlem12  33096  cdleme18d  33780  cdleme22b  33827  cdleme32e  33931  lclkrlem2e  34998  pell1234qrdich  35627  suctrALT  37083  wallispilem3  37749  bgoldbtbnd  38616