Theorem mpjaod 859

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

Syntax hints:   → wi 4   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  ecase2dOLD  1030  opth1  5476  onun2  6473  sorpssun  7720  sorpssin  7721  omun  7878  poxp2  8129  poxp3  8136  reldmtpos  8219  dftpos4  8230  oaass  8561  nnawordex  8637  omabs  8650  suplub2  9456  en3lplem2  9608  cantnflt  9667  cantnfp1lem3  9675  ttrclselem2  9721  tcrank  9879  cardaleph  10084  fpwwe2  10638  gchpwdom  10665  grur1  10815  indpi  10902  nn1suc  12234  nnsub  12256  seqid  14013  seqz  14016  faclbnd  14250  facavg  14261  bcval5  14278  hashnnn0genn0  14303  hashfzo  14389  01sqrexlem6  15194  resqrex  15197  absmod0  15250  absz  15258  iserex  15603  fsumf1o  15669  fsumss  15671  fsumcl2lem  15677  fsumadd  15686  fsummulc2  15730  fsumconst  15736  fsumrelem  15753  isumsplit  15786  fprodf1o  15890  fprodss  15892  fprodcl2lem  15894  fprodmul  15904  fproddiv  15905  fprodconst  15922  fprodn0  15923  absdvdsb  16218  dvdsabsb  16219  gcdabs1  16470  bezoutlem1  16481  bezoutlem2  16482  2mulprm  16630  isprm5  16644  pcabs  16808  pockthg  16839  prmreclem5  16853  vdwlem13  16926  0ram  16953  ram0  16955  prmlem0  17039  mulgnn0ass  18990  psgnunilem2  19363  mndodcongi  19411  oddvdsnn0  19412  odnncl  19413  efgredlemb  19614  gsumzres  19777  gsumzcl2  19778  gsumzf1o  19780  gsumzaddlem  19789  gsumconst  19802  gsumzmhm  19805  gsummulglem  19809  gsumzoppg  19812  pgpfac1lem5  19949  ablsimpnosubgd  19974  gsumfsum  21012  zringlpirlem1  21032  mplsubrglem  21563  ordthaus  22888  icccmplem2  24339  metdstri  24367  ioombl  25082  itgabs  25352  dvlip  25510  dvge0  25523  dvivthlem1  25525  dvcnvrelem1  25534  ply1rem  25681  dgrcolem2  25788  quotcan  25822  sinq12ge0  26018  argregt0  26118  argrege0  26119  scvxcvx  26490  bpos1lem  26785  bposlem3  26789  lgseisenlem2  26879  noextendseq  27170  nogt01o  27199  nosupprefixmo  27203  noinfprefixmo  27204  noinfbnd1lem5  27230  noetasuplem4  27239  noetainflem4  27243  frgrregord013  29679  htthlem  30201  atcvati  31670  ccatf1  32146  sinccvglem  34688  midofsegid  35107  outsideofeq  35133  hfun  35181  ordcmp  35380  icoreclin  36286  itgabsnc  36605  dvasin  36620  cvrat  38341  4atlem10  38525  4atlem12  38531  cdleme18d  39214  cdleme22b  39260  cdleme32e  39364  lclkrlem2e  40430  aks4d1p1  40989  pell1234qrdich  41647  onsupnmax  42025  omlimcl2  42039  onexlimgt  42040  onexoegt  42041  onsucf1olem  42068  oege1  42104  cantnfresb  42122  omabs2  42130  tfsconcat0b  42144  clsk1indlem3  42842  suctrALT  43635  wallispilem3  44831  bgoldbtbnd  46525  reorelicc  47444