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  5438  onun2  6445  sorpssun  7709  sorpssin  7710  omun  7867  poxp2  8125  poxp3  8132  reldmtpos  8216  dftpos4  8227  oaass  8528  nnawordex  8604  omabs  8618  suplub2  9419  en3lplem2  9573  cantnflt  9632  cantnfp1lem3  9640  ttrclselem2  9686  tcrank  9844  cardaleph  10049  fpwwe2  10603  gchpwdom  10630  grur1  10780  indpi  10867  nn1suc  12215  nnsub  12237  seqid  14019  seqz  14022  faclbnd  14262  facavg  14273  bcval5  14290  hashnnn0genn0  14315  hashfzo  14401  01sqrexlem6  15220  resqrex  15223  absmod0  15276  absz  15284  iserex  15630  fsumf1o  15696  fsumss  15698  fsumcl2lem  15704  fsumadd  15713  fsummulc2  15757  fsumconst  15763  fsumrelem  15780  isumsplit  15813  fprodf1o  15919  fprodss  15921  fprodcl2lem  15923  fprodmul  15933  fproddiv  15934  fprodconst  15951  fprodn0  15952  absdvdsb  16251  dvdsabsb  16252  gcdabs1  16506  bezoutlem1  16516  bezoutlem2  16517  2mulprm  16670  isprm5  16684  pcabs  16853  pockthg  16884  prmreclem5  16898  vdwlem13  16971  0ram  16998  ram0  17000  prmlem0  17083  mulgnn0ass  19049  psgnunilem2  19432  mndodcongi  19480  oddvdsnn0  19481  odnncl  19482  efgredlemb  19683  gsumzres  19846  gsumzcl2  19847  gsumzf1o  19849  gsumzaddlem  19858  gsumconst  19871  gsumzmhm  19874  gsummulglem  19878  gsumzoppg  19881  pgpfac1lem5  20018  ablsimpnosubgd  20043  gsumfsum  21358  zringlpirlem1  21379  mplsubrglem  21920  ordthaus  23278  icccmplem2  24719  metdstri  24747  ioombl  25473  itgabs  25743  dvlip  25905  dvge0  25918  dvivthlem1  25920  dvcnvrelem1  25929  ply1rem  26078  dgrcolem2  26187  quotcan  26224  sinq12ge0  26424  argregt0  26526  argrege0  26527  scvxcvx  26903  bpos1lem  27200  bposlem3  27204  lgseisenlem2  27294  noextendseq  27586  nogt01o  27615  nosupprefixmo  27619  noinfprefixmo  27620  noinfbnd1lem5  27646  noetasuplem4  27655  noetainflem4  27659  n0subs  28260  frgrregord013  30331  htthlem  30853  atcvati  32322  ccatf1  32877  sinccvglem  35666  midofsegid  36099  outsideofeq  36125  hfun  36173  ordcmp  36442  icoreclin  37352  itgabsnc  37690  dvasin  37705  cvrat  39423  4atlem10  39607  4atlem12  39613  cdleme18d  40296  cdleme22b  40342  cdleme32e  40446  lclkrlem2e  41512  aks4d1p1  42071  pell1234qrdich  42856  onsupnmax  43224  omlimcl2  43238  onexlimgt  43239  onexoegt  43240  onsucf1olem  43266  oege1  43302  cantnfresb  43320  omabs2  43328  tfsconcat0b  43342  clsk1indlem3  44039  suctrALT  44822  wallispilem3  46072  bgoldbtbnd  47814  reorelicc  48703  infsubc  49053  infsubc2  49054