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  29648  htthlem  30170  atcvati  31639  ccatf1  32115  sinccvglem  34657  midofsegid  35076  outsideofeq  35102  hfun  35150  ordcmp  35332  icoreclin  36238  itgabsnc  36557  dvasin  36572  cvrat  38293  4atlem10  38477  4atlem12  38483  cdleme18d  39166  cdleme22b  39212  cdleme32e  39316  lclkrlem2e  40382  aks4d1p1  40941  pell1234qrdich  41599  onsupnmax  41977  omlimcl2  41991  onexlimgt  41992  onexoegt  41993  onsucf1olem  42020  oege1  42056  cantnfresb  42074  omabs2  42082  tfsconcat0b  42096  clsk1indlem3  42794  suctrALT  43587  wallispilem3  44783  bgoldbtbnd  46477  reorelicc  47396