Theorem mpjaod 874

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 873	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
5	1, 4	mpd 16	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  opth1  5455  onun2  6472  sorpssun  7734  sorpssin  7735  omun  7887  poxp2  8144  poxp3  8151  reldmtpos  8235  dftpos4  8246  oaass  8551  nnawordex  8628  omabs  8642  suplub2  9434  en3lplem2  9595  cantnflt  9654  cantnfp1lem3  9662  ttrclselem2  9708  tcrank  9869  cardaleph  10095  fpwwe2  10655  gchpwdom  10682  grur1  10832  indpi  10919  nn1suc  12282  nnsub  12307  seqid  14113  seqz  14116  faclbnd  14356  facavg  14367  bcval5  14384  hashnnn0genn0  14409  hashfzo  14496  ccatf1  14658  01sqrexlem6  15336  resqrex  15339  absmod0  15392  absz  15400  iserex  15746  fsumf1o  15811  fsumss  15813  fsumcl2lem  15819  fsumadd  15828  fsummulc2  15872  fsumconst  15878  fsumrelem  15896  isumsplit  15931  fprodf1o  16037  fprodss  16039  fprodcl2lem  16041  fprodmul  16051  fproddiv  16052  fprodconst  16069  fprodn0  16070  absdvdsb  16368  dvdsabsb  16369  gcdabs1  16623  bezoutlem1  16633  bezoutlem2  16634  2mulprm  16787  isprm5  16802  pcabs  16971  pockthg  17002  prmreclem5  17016  vdwlem13  17089  0ram  17116  ram0  17118  prmlem0  17201  mulgnn0ass  19237  psgnunilem2  19626  mndodcongi  19674  oddvdsnn0  19675  odnncl  19676  efgredlemb  19877  gsumzres  20040  gsumzcl2  20041  gsumzf1o  20043  gsumzaddlem  20052  gsumconst  20065  gsumzmhm  20068  gsummulglem  20072  gsumzoppg  20075  pgpfac1lem5  20212  ablsimpnosubgd  20237  gsumfsum  21651  zringlpirlem1  21679  mplsubrglem  22222  ordthaus  23613  icccmplem2  25054  metdstri  25082  ioombl  25797  itgabs  26067  dvlip  26225  dvge0  26238  dvivthlem1  26240  dvcnvrelem1  26249  ply1rem  26396  dgrcolem2  26504  quotcan  26543  sinq12ge0  26746  argregt0  26848  argrege0  26849  scvxcvx  27223  bpos1lem  27519  bposlem3  27523  lgseisenlem2  27613  noextendseq  27904  nogt01o  27933  nosupprefixmo  27937  noinfprefixmo  27938  noinfbnd1lem5  27964  noetasuplem4  27973  noetainflem4  27977  n0subs  28629  bdayfinbndlem1  28733  bdayfinlem  28752  bdayfin  28753  frgrregord013  30876  htthlem  31399  atcvati  32868  sinccvglem  36253  midofsegid  36686  outsideofeq  36712  hfun  36760  ordcmp  37068  icoreclin  38113  itgabsnc  38440  dvasin  38455  cvrat  40297  4atlem10  40481  4atlem12  40487  cdleme18d  41170  cdleme22b  41216  cdleme32e  41320  lclkrlem2e  42386  aks4d1p1  42944  pell1234qrdich  43704  onsupnmax  44071  omlimcl2  44085  onexlimgt  44086  onexoegt  44087  onsucf1olem  44113  oege1  44149  cantnfresb  44167  omabs2  44175  tfsconcat0b  44189  clsk1indlem3  44885  suctrALT  45650  wallispilem3  46897  nprmmul2  48430  bgoldbtbnd  48727  reorelicc  49642  infsubc  49988  infsubc2  49989