Theorem mpjaod 869

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

Syntax hints:   → wi 4   ∨ wo 856

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 209  df-or 857

This theorem is referenced by:  opth1  5437  onun2  6445  sorpssun  7702  sorpssin  7703  omun  7857  poxp2  8111  poxp3  8118  reldmtpos  8202  dftpos4  8213  oaass  8518  nnawordex  8595  omabs  8609  suplub2  9397  en3lplem2  9558  cantnflt  9617  cantnfp1lem3  9625  ttrclselem2  9671  tcrank  9832  cardaleph  10035  fpwwe2  10591  gchpwdom  10618  grur1  10768  indpi  10855  nn1suc  12222  nnsub  12247  seqid  14050  seqz  14053  faclbnd  14293  facavg  14304  bcval5  14321  hashnnn0genn0  14346  hashfzo  14432  01sqrexlem6  15250  resqrex  15253  absmod0  15306  absz  15314  iserex  15660  fsumf1o  15726  fsumss  15728  fsumcl2lem  15734  fsumadd  15743  fsummulc2  15787  fsumconst  15793  fsumrelem  15811  isumsplit  15846  fprodf1o  15952  fprodss  15954  fprodcl2lem  15956  fprodmul  15966  fproddiv  15967  fprodconst  15984  fprodn0  15985  absdvdsb  16284  dvdsabsb  16285  gcdabs1  16539  bezoutlem1  16549  bezoutlem2  16550  2mulprm  16703  isprm5  16718  pcabs  16887  pockthg  16918  prmreclem5  16932  vdwlem13  17005  0ram  17032  ram0  17034  prmlem0  17117  mulgnn0ass  19128  psgnunilem2  19511  mndodcongi  19559  oddvdsnn0  19560  odnncl  19561  efgredlemb  19762  gsumzres  19925  gsumzcl2  19926  gsumzf1o  19928  gsumzaddlem  19937  gsumconst  19950  gsumzmhm  19953  gsummulglem  19957  gsumzoppg  19960  pgpfac1lem5  20097  ablsimpnosubgd  20122  gsumfsum  21459  zringlpirlem1  21487  mplsubrglem  22028  ordthaus  23417  icccmplem2  24857  metdstri  24885  ioombl  25600  itgabs  25870  dvlip  26028  dvge0  26041  dvivthlem1  26043  dvcnvrelem1  26052  ply1rem  26199  dgrcolem2  26307  quotcan  26343  sinq12ge0  26543  argregt0  26645  argrege0  26646  scvxcvx  27020  bpos1lem  27316  bposlem3  27320  lgseisenlem2  27410  noextendseq  27701  nogt01o  27730  nosupprefixmo  27734  noinfprefixmo  27735  noinfbnd1lem5  27761  noetasuplem4  27770  noetainflem4  27774  n0subs  28426  bdayfinbndlem1  28530  bdayfinlem  28549  bdayfin  28550  frgrregord013  30536  htthlem  31059  atcvati  32528  ccatf1  33081  sinccvglem  35970  midofsegid  36402  outsideofeq  36428  hfun  36476  ordcmp  36755  icoreclin  37799  itgabsnc  38136  dvasin  38151  cvrat  39994  4atlem10  40178  4atlem12  40184  cdleme18d  40867  cdleme22b  40913  cdleme32e  41017  lclkrlem2e  42083  aks4d1p1  42641  pell1234qrdich  43386  onsupnmax  43753  omlimcl2  43767  onexlimgt  43768  onexoegt  43769  onsucf1olem  43795  oege1  43831  cantnfresb  43849  omabs2  43857  tfsconcat0b  43871  clsk1indlem3  44567  suctrALT  45349  wallispilem3  46589  nprmmul2  48082  bgoldbtbnd  48379  reorelicc  49280  infsubc  49629  infsubc2  49630