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  5423  onun2  6427  sorpssun  7675  sorpssin  7676  omun  7830  poxp2  8085  poxp3  8092  reldmtpos  8176  dftpos4  8187  oaass  8488  nnawordex  8565  omabs  8579  suplub2  9364  en3lplem2  9522  cantnflt  9581  cantnfp1lem3  9589  ttrclselem2  9635  tcrank  9796  cardaleph  9999  fpwwe2  10554  gchpwdom  10581  grur1  10731  indpi  10818  nn1suc  12167  nnsub  12189  seqid  13970  seqz  13973  faclbnd  14213  facavg  14224  bcval5  14241  hashnnn0genn0  14266  hashfzo  14352  01sqrexlem6  15170  resqrex  15173  absmod0  15226  absz  15234  iserex  15580  fsumf1o  15646  fsumss  15648  fsumcl2lem  15654  fsumadd  15663  fsummulc2  15707  fsumconst  15713  fsumrelem  15730  isumsplit  15763  fprodf1o  15869  fprodss  15871  fprodcl2lem  15873  fprodmul  15883  fproddiv  15884  fprodconst  15901  fprodn0  15902  absdvdsb  16201  dvdsabsb  16202  gcdabs1  16456  bezoutlem1  16466  bezoutlem2  16467  2mulprm  16620  isprm5  16634  pcabs  16803  pockthg  16834  prmreclem5  16848  vdwlem13  16921  0ram  16948  ram0  16950  prmlem0  17033  mulgnn0ass  19040  psgnunilem2  19424  mndodcongi  19472  oddvdsnn0  19473  odnncl  19474  efgredlemb  19675  gsumzres  19838  gsumzcl2  19839  gsumzf1o  19841  gsumzaddlem  19850  gsumconst  19863  gsumzmhm  19866  gsummulglem  19870  gsumzoppg  19873  pgpfac1lem5  20010  ablsimpnosubgd  20035  gsumfsum  21389  zringlpirlem1  21417  mplsubrglem  21959  ordthaus  23328  icccmplem2  24768  metdstri  24796  ioombl  25522  itgabs  25792  dvlip  25954  dvge0  25967  dvivthlem1  25969  dvcnvrelem1  25978  ply1rem  26127  dgrcolem2  26236  quotcan  26273  sinq12ge0  26473  argregt0  26575  argrege0  26576  scvxcvx  26952  bpos1lem  27249  bposlem3  27253  lgseisenlem2  27343  noextendseq  27635  nogt01o  27664  nosupprefixmo  27668  noinfprefixmo  27669  noinfbnd1lem5  27695  noetasuplem4  27704  noetainflem4  27708  n0subs  28359  bdayfinbndlem1  28463  bdayfinlem  28482  bdayfin  28483  frgrregord013  30470  htthlem  30992  atcvati  32461  ccatf1  33031  sinccvglem  35866  midofsegid  36298  outsideofeq  36324  hfun  36372  ordcmp  36641  icoreclin  37562  itgabsnc  37890  dvasin  37905  cvrat  39682  4atlem10  39866  4atlem12  39872  cdleme18d  40555  cdleme22b  40601  cdleme32e  40705  lclkrlem2e  41771  aks4d1p1  42330  pell1234qrdich  43103  onsupnmax  43470  omlimcl2  43484  onexlimgt  43485  onexoegt  43486  onsucf1olem  43512  oege1  43548  cantnfresb  43566  omabs2  43574  tfsconcat0b  43588  clsk1indlem3  44284  suctrALT  45066  wallispilem3  46311  bgoldbtbnd  48055  reorelicc  48956  infsubc  49305  infsubc2  49306