Theorem mpjaod 873

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 860

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 861

This theorem is used by:  opth1  5456  onun2  6471  sorpssun  7729  sorpssin  7730  omun  7882  poxp2  8137  poxp3  8144  reldmtpos  8228  dftpos4  8239  oaass  8544  nnawordex  8621  omabs  8635  suplub2  9419  en3lplem2  9580  cantnflt  9639  cantnfp1lem3  9647  ttrclselem2  9693  tcrank  9854  cardaleph  10080  fpwwe2  10634  gchpwdom  10661  grur1  10811  indpi  10898  nn1suc  12261  nnsub  12286  seqid  14090  seqz  14093  faclbnd  14333  facavg  14344  bcval5  14361  hashnnn0genn0  14386  hashfzo  14473  01sqrexlem6  15305  resqrex  15308  absmod0  15361  absz  15369  iserex  15715  fsumf1o  15781  fsumss  15783  fsumcl2lem  15789  fsumadd  15798  fsummulc2  15842  fsumconst  15848  fsumrelem  15866  isumsplit  15901  fprodf1o  16007  fprodss  16009  fprodcl2lem  16011  fprodmul  16021  fproddiv  16022  fprodconst  16039  fprodn0  16040  absdvdsb  16338  dvdsabsb  16339  gcdabs1  16593  bezoutlem1  16603  bezoutlem2  16604  2mulprm  16757  isprm5  16772  pcabs  16941  pockthg  16972  prmreclem5  16986  vdwlem13  17059  0ram  17086  ram0  17088  prmlem0  17171  mulgnn0ass  19182  psgnunilem2  19571  mndodcongi  19619  oddvdsnn0  19620  odnncl  19621  efgredlemb  19822  gsumzres  19985  gsumzcl2  19986  gsumzf1o  19988  gsumzaddlem  19997  gsumconst  20010  gsumzmhm  20013  gsummulglem  20017  gsumzoppg  20020  pgpfac1lem5  20157  ablsimpnosubgd  20182  gsumfsum  21595  zringlpirlem1  21623  mplsubrglem  22164  ordthaus  23552  icccmplem2  24992  metdstri  25020  ioombl  25735  itgabs  26005  dvlip  26163  dvge0  26176  dvivthlem1  26178  dvcnvrelem1  26187  ply1rem  26334  dgrcolem2  26442  quotcan  26481  sinq12ge0  26684  argregt0  26786  argrege0  26787  scvxcvx  27161  bpos1lem  27457  bposlem3  27461  lgseisenlem2  27551  noextendseq  27842  nogt01o  27871  nosupprefixmo  27875  noinfprefixmo  27876  noinfbnd1lem5  27902  noetasuplem4  27911  noetainflem4  27915  n0subs  28567  bdayfinbndlem1  28671  bdayfinlem  28690  bdayfin  28691  frgrregord013  30757  htthlem  31280  atcvati  32749  ccatf1  33278  sinccvglem  36172  midofsegid  36604  outsideofeq  36630  hfun  36678  ordcmp  36986  icoreclin  38031  itgabsnc  38368  dvasin  38383  cvrat  40224  4atlem10  40408  4atlem12  40414  cdleme18d  41097  cdleme22b  41143  cdleme32e  41247  lclkrlem2e  42313  aks4d1p1  42871  pell1234qrdich  43616  onsupnmax  43983  omlimcl2  43997  onexlimgt  43998  onexoegt  43999  onsucf1olem  44025  oege1  44061  cantnfresb  44079  omabs2  44087  tfsconcat0b  44101  clsk1indlem3  44797  suctrALT  45562  wallispilem3  46809  nprmmul2  48305  bgoldbtbnd  48602  reorelicc  49518  infsubc  49866  infsubc2  49867