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

This theorem is referenced by:  ecase2dOLD  1031  opth1  5495  onun2  6503  sorpssun  7765  sorpssin  7766  omun  7926  poxp2  8184  poxp3  8191  reldmtpos  8275  dftpos4  8286  oaass  8617  nnawordex  8693  omabs  8707  suplub2  9530  en3lplem2  9682  cantnflt  9741  cantnfp1lem3  9749  ttrclselem2  9795  tcrank  9953  cardaleph  10158  fpwwe2  10712  gchpwdom  10739  grur1  10889  indpi  10976  nn1suc  12315  nnsub  12337  seqid  14098  seqz  14101  faclbnd  14339  facavg  14350  bcval5  14367  hashnnn0genn0  14392  hashfzo  14478  01sqrexlem6  15296  resqrex  15299  absmod0  15352  absz  15360  iserex  15705  fsumf1o  15771  fsumss  15773  fsumcl2lem  15779  fsumadd  15788  fsummulc2  15832  fsumconst  15838  fsumrelem  15855  isumsplit  15888  fprodf1o  15994  fprodss  15996  fprodcl2lem  15998  fprodmul  16008  fproddiv  16009  fprodconst  16026  fprodn0  16027  absdvdsb  16323  dvdsabsb  16324  gcdabs1  16575  bezoutlem1  16586  bezoutlem2  16587  2mulprm  16740  isprm5  16754  pcabs  16922  pockthg  16953  prmreclem5  16967  vdwlem13  17040  0ram  17067  ram0  17069  prmlem0  17153  mulgnn0ass  19150  psgnunilem2  19537  mndodcongi  19585  oddvdsnn0  19586  odnncl  19587  efgredlemb  19788  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumconst  19976  gsumzmhm  19979  gsummulglem  19983  gsumzoppg  19986  pgpfac1lem5  20123  ablsimpnosubgd  20148  gsumfsum  21475  zringlpirlem1  21496  mplsubrglem  22047  ordthaus  23413  icccmplem2  24864  metdstri  24892  ioombl  25619  itgabs  25890  dvlip  26052  dvge0  26065  dvivthlem1  26067  dvcnvrelem1  26076  ply1rem  26225  dgrcolem2  26334  quotcan  26369  sinq12ge0  26568  argregt0  26670  argrege0  26671  scvxcvx  27047  bpos1lem  27344  bposlem3  27348  lgseisenlem2  27438  noextendseq  27730  nogt01o  27759  nosupprefixmo  27763  noinfprefixmo  27764  noinfbnd1lem5  27790  noetasuplem4  27799  noetainflem4  27803  n0subs  28378  frgrregord013  30427  htthlem  30949  atcvati  32418  ccatf1  32915  sinccvglem  35640  midofsegid  36068  outsideofeq  36094  hfun  36142  ordcmp  36413  icoreclin  37323  itgabsnc  37649  dvasin  37664  cvrat  39379  4atlem10  39563  4atlem12  39569  cdleme18d  40252  cdleme22b  40298  cdleme32e  40402  lclkrlem2e  41468  aks4d1p1  42033  pell1234qrdich  42817  onsupnmax  43189  omlimcl2  43203  onexlimgt  43204  onexoegt  43205  onsucf1olem  43232  oege1  43268  cantnfresb  43286  omabs2  43294  tfsconcat0b  43308  clsk1indlem3  44005  suctrALT  44797  wallispilem3  45988  bgoldbtbnd  47683  reorelicc  48444