Theorem mpjaod 861

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  opth1  5431  onun2  6435  sorpssun  7685  sorpssin  7686  omun  7840  poxp2  8095  poxp3  8102  reldmtpos  8186  dftpos4  8197  oaass  8498  nnawordex  8575  omabs  8589  suplub2  9376  en3lplem2  9534  cantnflt  9593  cantnfp1lem3  9601  ttrclselem2  9647  tcrank  9808  cardaleph  10011  fpwwe2  10566  gchpwdom  10593  grur1  10743  indpi  10830  nn1suc  12179  nnsub  12201  seqid  13982  seqz  13985  faclbnd  14225  facavg  14236  bcval5  14253  hashnnn0genn0  14278  hashfzo  14364  01sqrexlem6  15182  resqrex  15185  absmod0  15238  absz  15246  iserex  15592  fsumf1o  15658  fsumss  15660  fsumcl2lem  15666  fsumadd  15675  fsummulc2  15719  fsumconst  15725  fsumrelem  15742  isumsplit  15775  fprodf1o  15881  fprodss  15883  fprodcl2lem  15885  fprodmul  15895  fproddiv  15896  fprodconst  15913  fprodn0  15914  absdvdsb  16213  dvdsabsb  16214  gcdabs1  16468  bezoutlem1  16478  bezoutlem2  16479  2mulprm  16632  isprm5  16646  pcabs  16815  pockthg  16846  prmreclem5  16860  vdwlem13  16933  0ram  16960  ram0  16962  prmlem0  17045  mulgnn0ass  19052  psgnunilem2  19436  mndodcongi  19484  oddvdsnn0  19485  odnncl  19486  efgredlemb  19687  gsumzres  19850  gsumzcl2  19851  gsumzf1o  19853  gsumzaddlem  19862  gsumconst  19875  gsumzmhm  19878  gsummulglem  19882  gsumzoppg  19885  pgpfac1lem5  20022  ablsimpnosubgd  20047  gsumfsum  21401  zringlpirlem1  21429  mplsubrglem  21971  ordthaus  23340  icccmplem2  24780  metdstri  24808  ioombl  25534  itgabs  25804  dvlip  25966  dvge0  25979  dvivthlem1  25981  dvcnvrelem1  25990  ply1rem  26139  dgrcolem2  26248  quotcan  26285  sinq12ge0  26485  argregt0  26587  argrege0  26588  scvxcvx  26964  bpos1lem  27261  bposlem3  27265  lgseisenlem2  27355  noextendseq  27647  nogt01o  27676  nosupprefixmo  27680  noinfprefixmo  27681  noinfbnd1lem5  27707  noetasuplem4  27716  noetainflem4  27720  n0subs  28371  bdayfinbndlem1  28475  bdayfinlem  28494  bdayfin  28495  frgrregord013  30482  htthlem  31004  atcvati  32473  ccatf1  33041  sinccvglem  35885  midofsegid  36317  outsideofeq  36343  hfun  36391  ordcmp  36660  icoreclin  37601  itgabsnc  37929  dvasin  37944  cvrat  39787  4atlem10  39971  4atlem12  39977  cdleme18d  40660  cdleme22b  40706  cdleme32e  40810  lclkrlem2e  41876  aks4d1p1  42435  pell1234qrdich  43207  onsupnmax  43574  omlimcl2  43588  onexlimgt  43589  onexoegt  43590  onsucf1olem  43616  oege1  43652  cantnfresb  43670  omabs2  43678  tfsconcat0b  43692  clsk1indlem3  44388  suctrALT  45170  wallispilem3  46414  bgoldbtbnd  48158  reorelicc  49059  infsubc  49408  infsubc2  49409