Theorem mpjaod 860

Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)

Hypotheses

Ref	Expression
jaod.1	⊢ (𝜑 → (𝜓 → 𝜒))
jaod.2	⊢ (𝜑 → (𝜃 → 𝜒))
jaod.3	⊢ (𝜑 → (𝜓 ∨ 𝜃))

Assertion

Ref	Expression
mpjaod	⊢ (𝜑 → 𝜒)

Proof of Theorem mpjaod

Step	Hyp	Ref	Expression
1		jaod.3	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃))
2		jaod.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaod.2	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
4	2, 3	jaod 859	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  opth1  5486  onun2  6494  sorpssun  7749  sorpssin  7750  omun  7910  poxp2  8167  poxp3  8174  reldmtpos  8258  dftpos4  8269  oaass  8598  nnawordex  8674  omabs  8688  suplub2  9499  en3lplem2  9651  cantnflt  9710  cantnfp1lem3  9718  ttrclselem2  9764  tcrank  9922  cardaleph  10127  fpwwe2  10681  gchpwdom  10708  grur1  10858  indpi  10945  nn1suc  12286  nnsub  12308  seqid  14085  seqz  14088  faclbnd  14326  facavg  14337  bcval5  14354  hashnnn0genn0  14379  hashfzo  14465  01sqrexlem6  15283  resqrex  15286  absmod0  15339  absz  15347  iserex  15690  fsumf1o  15756  fsumss  15758  fsumcl2lem  15764  fsumadd  15773  fsummulc2  15817  fsumconst  15823  fsumrelem  15840  isumsplit  15873  fprodf1o  15979  fprodss  15981  fprodcl2lem  15983  fprodmul  15993  fproddiv  15994  fprodconst  16011  fprodn0  16012  absdvdsb  16309  dvdsabsb  16310  gcdabs1  16563  bezoutlem1  16573  bezoutlem2  16574  2mulprm  16727  isprm5  16741  pcabs  16909  pockthg  16940  prmreclem5  16954  vdwlem13  17027  0ram  17054  ram0  17056  prmlem0  17140  mulgnn0ass  19141  psgnunilem2  19528  mndodcongi  19576  oddvdsnn0  19577  odnncl  19578  efgredlemb  19779  gsumzres  19942  gsumzcl2  19943  gsumzf1o  19945  gsumzaddlem  19954  gsumconst  19967  gsumzmhm  19970  gsummulglem  19974  gsumzoppg  19977  pgpfac1lem5  20114  ablsimpnosubgd  20139  gsumfsum  21470  zringlpirlem1  21491  mplsubrglem  22042  ordthaus  23408  icccmplem2  24859  metdstri  24887  ioombl  25614  itgabs  25885  dvlip  26047  dvge0  26060  dvivthlem1  26062  dvcnvrelem1  26071  ply1rem  26220  dgrcolem2  26329  quotcan  26366  sinq12ge0  26565  argregt0  26667  argrege0  26668  scvxcvx  27044  bpos1lem  27341  bposlem3  27345  lgseisenlem2  27435  noextendseq  27727  nogt01o  27756  nosupprefixmo  27760  noinfprefixmo  27761  noinfbnd1lem5  27787  noetasuplem4  27796  noetainflem4  27800  n0subs  28375  frgrregord013  30424  htthlem  30946  atcvati  32415  ccatf1  32918  sinccvglem  35657  midofsegid  36086  outsideofeq  36112  hfun  36160  ordcmp  36430  icoreclin  37340  itgabsnc  37676  dvasin  37691  cvrat  39405  4atlem10  39589  4atlem12  39595  cdleme18d  40278  cdleme22b  40324  cdleme32e  40428  lclkrlem2e  41494  aks4d1p1  42058  pell1234qrdich  42849  onsupnmax  43217  omlimcl2  43231  onexlimgt  43232  onexoegt  43233  onsucf1olem  43260  oege1  43296  cantnfresb  43314  omabs2  43322  tfsconcat0b  43336  clsk1indlem3  44033  suctrALT  44824  wallispilem3  46023  bgoldbtbnd  47734  reorelicc  48560