Theorem mpjaod 861

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  opth1  5424  onun2  6428  sorpssun  7677  sorpssin  7678  omun  7832  poxp2  8087  poxp3  8094  reldmtpos  8178  dftpos4  8189  oaass  8490  nnawordex  8567  omabs  8581  suplub2  9368  en3lplem2  9526  cantnflt  9585  cantnfp1lem3  9593  ttrclselem2  9639  tcrank  9800  cardaleph  10003  fpwwe2  10558  gchpwdom  10585  grur1  10735  indpi  10822  nn1suc  12171  nnsub  12193  seqid  13974  seqz  13977  faclbnd  14217  facavg  14228  bcval5  14245  hashnnn0genn0  14270  hashfzo  14356  01sqrexlem6  15174  resqrex  15177  absmod0  15230  absz  15238  iserex  15584  fsumf1o  15650  fsumss  15652  fsumcl2lem  15658  fsumadd  15667  fsummulc2  15711  fsumconst  15717  fsumrelem  15734  isumsplit  15767  fprodf1o  15873  fprodss  15875  fprodcl2lem  15877  fprodmul  15887  fproddiv  15888  fprodconst  15905  fprodn0  15906  absdvdsb  16205  dvdsabsb  16206  gcdabs1  16460  bezoutlem1  16470  bezoutlem2  16471  2mulprm  16624  isprm5  16638  pcabs  16807  pockthg  16838  prmreclem5  16852  vdwlem13  16925  0ram  16952  ram0  16954  prmlem0  17037  mulgnn0ass  19044  psgnunilem2  19428  mndodcongi  19476  oddvdsnn0  19477  odnncl  19478  efgredlemb  19679  gsumzres  19842  gsumzcl2  19843  gsumzf1o  19845  gsumzaddlem  19854  gsumconst  19867  gsumzmhm  19870  gsummulglem  19874  gsumzoppg  19877  pgpfac1lem5  20014  ablsimpnosubgd  20039  gsumfsum  21393  zringlpirlem1  21421  mplsubrglem  21963  ordthaus  23332  icccmplem2  24772  metdstri  24800  ioombl  25526  itgabs  25796  dvlip  25958  dvge0  25971  dvivthlem1  25973  dvcnvrelem1  25982  ply1rem  26131  dgrcolem2  26240  quotcan  26277  sinq12ge0  26477  argregt0  26579  argrege0  26580  scvxcvx  26956  bpos1lem  27253  bposlem3  27257  lgseisenlem2  27347  noextendseq  27639  nogt01o  27668  nosupprefixmo  27672  noinfprefixmo  27673  noinfbnd1lem5  27699  noetasuplem4  27708  noetainflem4  27712  n0subs  28342  bdayfinbndlem1  28446  bdayfinlem  28465  bdayfin  28466  frgrregord013  30453  htthlem  30975  atcvati  32444  ccatf1  33012  sinccvglem  35847  midofsegid  36279  outsideofeq  36305  hfun  36353  ordcmp  36622  icoreclin  37533  itgabsnc  37861  dvasin  37876  cvrat  39719  4atlem10  39903  4atlem12  39909  cdleme18d  40592  cdleme22b  40638  cdleme32e  40742  lclkrlem2e  41808  aks4d1p1  42367  pell1234qrdich  43139  onsupnmax  43506  omlimcl2  43520  onexlimgt  43521  onexoegt  43522  onsucf1olem  43548  oege1  43584  cantnfresb  43602  omabs2  43610  tfsconcat0b  43624  clsk1indlem3  44320  suctrALT  45102  wallispilem3  46347  bgoldbtbnd  48091  reorelicc  48992  infsubc  49341  infsubc2  49342