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  5413  onun2  6412  sorpssun  7658  sorpssin  7659  omun  7813  poxp2  8068  poxp3  8075  reldmtpos  8159  dftpos4  8170  oaass  8471  nnawordex  8547  omabs  8561  suplub2  9340  en3lplem2  9498  cantnflt  9557  cantnfp1lem3  9565  ttrclselem2  9611  tcrank  9769  cardaleph  9972  fpwwe2  10526  gchpwdom  10553  grur1  10703  indpi  10790  nn1suc  12139  nnsub  12161  seqid  13946  seqz  13949  faclbnd  14189  facavg  14200  bcval5  14217  hashnnn0genn0  14242  hashfzo  14328  01sqrexlem6  15146  resqrex  15149  absmod0  15202  absz  15210  iserex  15556  fsumf1o  15622  fsumss  15624  fsumcl2lem  15630  fsumadd  15639  fsummulc2  15683  fsumconst  15689  fsumrelem  15706  isumsplit  15739  fprodf1o  15845  fprodss  15847  fprodcl2lem  15849  fprodmul  15859  fproddiv  15860  fprodconst  15877  fprodn0  15878  absdvdsb  16177  dvdsabsb  16178  gcdabs1  16432  bezoutlem1  16442  bezoutlem2  16443  2mulprm  16596  isprm5  16610  pcabs  16779  pockthg  16810  prmreclem5  16824  vdwlem13  16897  0ram  16924  ram0  16926  prmlem0  17009  mulgnn0ass  19015  psgnunilem2  19400  mndodcongi  19448  oddvdsnn0  19449  odnncl  19450  efgredlemb  19651  gsumzres  19814  gsumzcl2  19815  gsumzf1o  19817  gsumzaddlem  19826  gsumconst  19839  gsumzmhm  19842  gsummulglem  19846  gsumzoppg  19849  pgpfac1lem5  19986  ablsimpnosubgd  20011  gsumfsum  21364  zringlpirlem1  21392  mplsubrglem  21934  ordthaus  23292  icccmplem2  24732  metdstri  24760  ioombl  25486  itgabs  25756  dvlip  25918  dvge0  25931  dvivthlem1  25933  dvcnvrelem1  25942  ply1rem  26091  dgrcolem2  26200  quotcan  26237  sinq12ge0  26437  argregt0  26539  argrege0  26540  scvxcvx  26916  bpos1lem  27213  bposlem3  27217  lgseisenlem2  27307  noextendseq  27599  nogt01o  27628  nosupprefixmo  27632  noinfprefixmo  27633  noinfbnd1lem5  27659  noetasuplem4  27668  noetainflem4  27672  n0subs  28282  frgrregord013  30365  htthlem  30887  atcvati  32356  ccatf1  32920  sinccvglem  35684  midofsegid  36117  outsideofeq  36143  hfun  36191  ordcmp  36460  icoreclin  37370  itgabsnc  37708  dvasin  37723  cvrat  39440  4atlem10  39624  4atlem12  39630  cdleme18d  40313  cdleme22b  40359  cdleme32e  40463  lclkrlem2e  41529  aks4d1p1  42088  pell1234qrdich  42873  onsupnmax  43240  omlimcl2  43254  onexlimgt  43255  onexoegt  43256  onsucf1olem  43282  oege1  43318  cantnfresb  43336  omabs2  43344  tfsconcat0b  43358  clsk1indlem3  44055  suctrALT  44837  wallispilem3  46084  bgoldbtbnd  47819  reorelicc  48721  infsubc  49071  infsubc2  49072