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  5422  onun2  6421  sorpssun  7670  sorpssin  7671  omun  7828  poxp2  8083  poxp3  8090  reldmtpos  8174  dftpos4  8185  oaass  8486  nnawordex  8562  omabs  8576  suplub2  9370  en3lplem2  9528  cantnflt  9587  cantnfp1lem3  9595  ttrclselem2  9641  tcrank  9799  cardaleph  10002  fpwwe2  10556  gchpwdom  10583  grur1  10733  indpi  10820  nn1suc  12168  nnsub  12190  seqid  13972  seqz  13975  faclbnd  14215  facavg  14226  bcval5  14243  hashnnn0genn0  14268  hashfzo  14354  01sqrexlem6  15172  resqrex  15175  absmod0  15228  absz  15236  iserex  15582  fsumf1o  15648  fsumss  15650  fsumcl2lem  15656  fsumadd  15665  fsummulc2  15709  fsumconst  15715  fsumrelem  15732  isumsplit  15765  fprodf1o  15871  fprodss  15873  fprodcl2lem  15875  fprodmul  15885  fproddiv  15886  fprodconst  15903  fprodn0  15904  absdvdsb  16203  dvdsabsb  16204  gcdabs1  16458  bezoutlem1  16468  bezoutlem2  16469  2mulprm  16622  isprm5  16636  pcabs  16805  pockthg  16836  prmreclem5  16850  vdwlem13  16923  0ram  16950  ram0  16952  prmlem0  17035  mulgnn0ass  19007  psgnunilem2  19392  mndodcongi  19440  oddvdsnn0  19441  odnncl  19442  efgredlemb  19643  gsumzres  19806  gsumzcl2  19807  gsumzf1o  19809  gsumzaddlem  19818  gsumconst  19831  gsumzmhm  19834  gsummulglem  19838  gsumzoppg  19841  pgpfac1lem5  19978  ablsimpnosubgd  20003  gsumfsum  21359  zringlpirlem1  21387  mplsubrglem  21929  ordthaus  23287  icccmplem2  24728  metdstri  24756  ioombl  25482  itgabs  25752  dvlip  25914  dvge0  25927  dvivthlem1  25929  dvcnvrelem1  25938  ply1rem  26087  dgrcolem2  26196  quotcan  26233  sinq12ge0  26433  argregt0  26535  argrege0  26536  scvxcvx  26912  bpos1lem  27209  bposlem3  27213  lgseisenlem2  27303  noextendseq  27595  nogt01o  27624  nosupprefixmo  27628  noinfprefixmo  27629  noinfbnd1lem5  27655  noetasuplem4  27664  noetainflem4  27668  n0subs  28276  frgrregord013  30357  htthlem  30879  atcvati  32348  ccatf1  32903  sinccvglem  35644  midofsegid  36077  outsideofeq  36103  hfun  36151  ordcmp  36420  icoreclin  37330  itgabsnc  37668  dvasin  37683  cvrat  39401  4atlem10  39585  4atlem12  39591  cdleme18d  40274  cdleme22b  40320  cdleme32e  40424  lclkrlem2e  41490  aks4d1p1  42049  pell1234qrdich  42834  onsupnmax  43201  omlimcl2  43215  onexlimgt  43216  onexoegt  43217  onsucf1olem  43243  oege1  43279  cantnfresb  43297  omabs2  43305  tfsconcat0b  43319  clsk1indlem3  44016  suctrALT  44799  wallispilem3  46049  bgoldbtbnd  47794  reorelicc  48683  infsubc  49033  infsubc2  49034