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  5450  onun2  6462  sorpssun  7724  sorpssin  7725  omun  7883  poxp2  8142  poxp3  8149  reldmtpos  8233  dftpos4  8244  oaass  8573  nnawordex  8649  omabs  8663  suplub2  9473  en3lplem2  9627  cantnflt  9686  cantnfp1lem3  9694  ttrclselem2  9740  tcrank  9898  cardaleph  10103  fpwwe2  10657  gchpwdom  10684  grur1  10834  indpi  10921  nn1suc  12262  nnsub  12284  seqid  14065  seqz  14068  faclbnd  14308  facavg  14319  bcval5  14336  hashnnn0genn0  14361  hashfzo  14447  01sqrexlem6  15266  resqrex  15269  absmod0  15322  absz  15330  iserex  15673  fsumf1o  15739  fsumss  15741  fsumcl2lem  15747  fsumadd  15756  fsummulc2  15800  fsumconst  15806  fsumrelem  15823  isumsplit  15856  fprodf1o  15962  fprodss  15964  fprodcl2lem  15966  fprodmul  15976  fproddiv  15977  fprodconst  15994  fprodn0  15995  absdvdsb  16294  dvdsabsb  16295  gcdabs1  16548  bezoutlem1  16558  bezoutlem2  16559  2mulprm  16712  isprm5  16726  pcabs  16895  pockthg  16926  prmreclem5  16940  vdwlem13  17013  0ram  17040  ram0  17042  prmlem0  17125  mulgnn0ass  19093  psgnunilem2  19476  mndodcongi  19524  oddvdsnn0  19525  odnncl  19526  efgredlemb  19727  gsumzres  19890  gsumzcl2  19891  gsumzf1o  19893  gsumzaddlem  19902  gsumconst  19915  gsumzmhm  19918  gsummulglem  19922  gsumzoppg  19925  pgpfac1lem5  20062  ablsimpnosubgd  20087  gsumfsum  21402  zringlpirlem1  21423  mplsubrglem  21964  ordthaus  23322  icccmplem2  24763  metdstri  24791  ioombl  25518  itgabs  25788  dvlip  25950  dvge0  25963  dvivthlem1  25965  dvcnvrelem1  25974  ply1rem  26123  dgrcolem2  26232  quotcan  26269  sinq12ge0  26469  argregt0  26571  argrege0  26572  scvxcvx  26948  bpos1lem  27245  bposlem3  27249  lgseisenlem2  27339  noextendseq  27631  nogt01o  27660  nosupprefixmo  27664  noinfprefixmo  27665  noinfbnd1lem5  27691  noetasuplem4  27700  noetainflem4  27704  n0subs  28305  frgrregord013  30376  htthlem  30898  atcvati  32367  ccatf1  32924  sinccvglem  35694  midofsegid  36122  outsideofeq  36148  hfun  36196  ordcmp  36465  icoreclin  37375  itgabsnc  37713  dvasin  37728  cvrat  39441  4atlem10  39625  4atlem12  39631  cdleme18d  40314  cdleme22b  40360  cdleme32e  40464  lclkrlem2e  41530  aks4d1p1  42089  pell1234qrdich  42884  onsupnmax  43252  omlimcl2  43266  onexlimgt  43267  onexoegt  43268  onsucf1olem  43294  oege1  43330  cantnfresb  43348  omabs2  43356  tfsconcat0b  43370  clsk1indlem3  44067  suctrALT  44850  wallispilem3  46096  bgoldbtbnd  47823  reorelicc  48690  infsubc  49027  infsubc2  49028