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  5435  onun2  6442  sorpssun  7706  sorpssin  7707  omun  7864  poxp2  8122  poxp3  8129  reldmtpos  8213  dftpos4  8224  oaass  8525  nnawordex  8601  omabs  8615  suplub2  9412  en3lplem2  9566  cantnflt  9625  cantnfp1lem3  9633  ttrclselem2  9679  tcrank  9837  cardaleph  10042  fpwwe2  10596  gchpwdom  10623  grur1  10773  indpi  10860  nn1suc  12208  nnsub  12230  seqid  14012  seqz  14015  faclbnd  14255  facavg  14266  bcval5  14283  hashnnn0genn0  14308  hashfzo  14394  01sqrexlem6  15213  resqrex  15216  absmod0  15269  absz  15277  iserex  15623  fsumf1o  15689  fsumss  15691  fsumcl2lem  15697  fsumadd  15706  fsummulc2  15750  fsumconst  15756  fsumrelem  15773  isumsplit  15806  fprodf1o  15912  fprodss  15914  fprodcl2lem  15916  fprodmul  15926  fproddiv  15927  fprodconst  15944  fprodn0  15945  absdvdsb  16244  dvdsabsb  16245  gcdabs1  16499  bezoutlem1  16509  bezoutlem2  16510  2mulprm  16663  isprm5  16677  pcabs  16846  pockthg  16877  prmreclem5  16891  vdwlem13  16964  0ram  16991  ram0  16993  prmlem0  17076  mulgnn0ass  19042  psgnunilem2  19425  mndodcongi  19473  oddvdsnn0  19474  odnncl  19475  efgredlemb  19676  gsumzres  19839  gsumzcl2  19840  gsumzf1o  19842  gsumzaddlem  19851  gsumconst  19864  gsumzmhm  19867  gsummulglem  19871  gsumzoppg  19874  pgpfac1lem5  20011  ablsimpnosubgd  20036  gsumfsum  21351  zringlpirlem1  21372  mplsubrglem  21913  ordthaus  23271  icccmplem2  24712  metdstri  24740  ioombl  25466  itgabs  25736  dvlip  25898  dvge0  25911  dvivthlem1  25913  dvcnvrelem1  25922  ply1rem  26071  dgrcolem2  26180  quotcan  26217  sinq12ge0  26417  argregt0  26519  argrege0  26520  scvxcvx  26896  bpos1lem  27193  bposlem3  27197  lgseisenlem2  27287  noextendseq  27579  nogt01o  27608  nosupprefixmo  27612  noinfprefixmo  27613  noinfbnd1lem5  27639  noetasuplem4  27648  noetainflem4  27652  n0subs  28253  frgrregord013  30324  htthlem  30846  atcvati  32315  ccatf1  32870  sinccvglem  35659  midofsegid  36092  outsideofeq  36118  hfun  36166  ordcmp  36435  icoreclin  37345  itgabsnc  37683  dvasin  37698  cvrat  39416  4atlem10  39600  4atlem12  39606  cdleme18d  40289  cdleme22b  40335  cdleme32e  40439  lclkrlem2e  41505  aks4d1p1  42064  pell1234qrdich  42849  onsupnmax  43217  omlimcl2  43231  onexlimgt  43232  onexoegt  43233  onsucf1olem  43259  oege1  43295  cantnfresb  43313  omabs2  43321  tfsconcat0b  43335  clsk1indlem3  44032  suctrALT  44815  wallispilem3  46065  bgoldbtbnd  47810  reorelicc  48699  infsubc  49049  infsubc2  49050