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  5420  onun2  6424  sorpssun  7672  sorpssin  7673  omun  7827  poxp2  8082  poxp3  8089  reldmtpos  8173  dftpos4  8184  oaass  8485  nnawordex  8561  omabs  8575  suplub2  9355  en3lplem2  9513  cantnflt  9572  cantnfp1lem3  9580  ttrclselem2  9626  tcrank  9787  cardaleph  9990  fpwwe2  10544  gchpwdom  10571  grur1  10721  indpi  10808  nn1suc  12157  nnsub  12179  seqid  13964  seqz  13967  faclbnd  14207  facavg  14218  bcval5  14235  hashnnn0genn0  14260  hashfzo  14346  01sqrexlem6  15164  resqrex  15167  absmod0  15220  absz  15228  iserex  15574  fsumf1o  15640  fsumss  15642  fsumcl2lem  15648  fsumadd  15657  fsummulc2  15701  fsumconst  15707  fsumrelem  15724  isumsplit  15757  fprodf1o  15863  fprodss  15865  fprodcl2lem  15867  fprodmul  15877  fproddiv  15878  fprodconst  15895  fprodn0  15896  absdvdsb  16195  dvdsabsb  16196  gcdabs1  16450  bezoutlem1  16460  bezoutlem2  16461  2mulprm  16614  isprm5  16628  pcabs  16797  pockthg  16828  prmreclem5  16842  vdwlem13  16915  0ram  16942  ram0  16944  prmlem0  17027  mulgnn0ass  19033  psgnunilem2  19417  mndodcongi  19465  oddvdsnn0  19466  odnncl  19467  efgredlemb  19668  gsumzres  19831  gsumzcl2  19832  gsumzf1o  19834  gsumzaddlem  19843  gsumconst  19856  gsumzmhm  19859  gsummulglem  19863  gsumzoppg  19866  pgpfac1lem5  20003  ablsimpnosubgd  20028  gsumfsum  21381  zringlpirlem1  21409  mplsubrglem  21951  ordthaus  23309  icccmplem2  24749  metdstri  24777  ioombl  25503  itgabs  25773  dvlip  25935  dvge0  25948  dvivthlem1  25950  dvcnvrelem1  25959  ply1rem  26108  dgrcolem2  26217  quotcan  26254  sinq12ge0  26454  argregt0  26556  argrege0  26557  scvxcvx  26933  bpos1lem  27230  bposlem3  27234  lgseisenlem2  27324  noextendseq  27616  nogt01o  27645  nosupprefixmo  27649  noinfprefixmo  27650  noinfbnd1lem5  27676  noetasuplem4  27685  noetainflem4  27689  n0subs  28299  frgrregord013  30386  htthlem  30908  atcvati  32377  ccatf1  32941  sinccvglem  35727  midofsegid  36159  outsideofeq  36185  hfun  36233  ordcmp  36502  icoreclin  37412  itgabsnc  37739  dvasin  37754  cvrat  39531  4atlem10  39715  4atlem12  39721  cdleme18d  40404  cdleme22b  40450  cdleme32e  40554  lclkrlem2e  41620  aks4d1p1  42179  pell1234qrdich  42968  onsupnmax  43335  omlimcl2  43349  onexlimgt  43350  onexoegt  43351  onsucf1olem  43377  oege1  43413  cantnfresb  43431  omabs2  43439  tfsconcat0b  43453  clsk1indlem3  44150  suctrALT  44932  wallispilem3  46179  bgoldbtbnd  47923  reorelicc  48825  infsubc  49175  infsubc2  49176