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 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  opth1  5457  onun2  6471  sorpssun  7727  sorpssin  7728  omun  7883  poxp2  8138  poxp3  8145  reldmtpos  8229  dftpos4  8240  oaass  8545  nnawordex  8622  omabs  8636  suplub2  9420  en3lplem2  9581  cantnflt  9640  cantnfp1lem3  9648  ttrclselem2  9694  tcrank  9855  cardaleph  10072  fpwwe2  10627  gchpwdom  10654  grur1  10804  indpi  10891  nn1suc  12254  nnsub  12279  seqid  14083  seqz  14086  faclbnd  14326  facavg  14337  bcval5  14354  hashnnn0genn0  14379  hashfzo  14466  01sqrexlem6  15298  resqrex  15301  absmod0  15354  absz  15362  iserex  15708  fsumf1o  15774  fsumss  15776  fsumcl2lem  15782  fsumadd  15791  fsummulc2  15835  fsumconst  15841  fsumrelem  15859  isumsplit  15894  fprodf1o  16000  fprodss  16002  fprodcl2lem  16004  fprodmul  16014  fproddiv  16015  fprodconst  16032  fprodn0  16033  absdvdsb  16331  dvdsabsb  16332  gcdabs1  16586  bezoutlem1  16596  bezoutlem2  16597  2mulprm  16750  isprm5  16765  pcabs  16934  pockthg  16965  prmreclem5  16979  vdwlem13  17052  0ram  17079  ram0  17081  prmlem0  17164  mulgnn0ass  19175  psgnunilem2  19564  mndodcongi  19612  oddvdsnn0  19613  odnncl  19614  efgredlemb  19815  gsumzres  19978  gsumzcl2  19979  gsumzf1o  19981  gsumzaddlem  19990  gsumconst  20003  gsumzmhm  20006  gsummulglem  20010  gsumzoppg  20013  pgpfac1lem5  20150  ablsimpnosubgd  20175  gsumfsum  21563  zringlpirlem1  21591  mplsubrglem  22132  ordthaus  23520  icccmplem2  24960  metdstri  24988  ioombl  25703  itgabs  25973  dvlip  26131  dvge0  26144  dvivthlem1  26146  dvcnvrelem1  26155  ply1rem  26302  dgrcolem2  26410  quotcan  26449  sinq12ge0  26649  argregt0  26751  argrege0  26752  scvxcvx  27126  bpos1lem  27422  bposlem3  27426  lgseisenlem2  27516  noextendseq  27807  nogt01o  27836  nosupprefixmo  27840  noinfprefixmo  27841  noinfbnd1lem5  27867  noetasuplem4  27876  noetainflem4  27880  n0subs  28532  bdayfinbndlem1  28636  bdayfinlem  28655  bdayfin  28656  frgrregord013  30712  htthlem  31235  atcvati  32704  ccatf1  33235  sinccvglem  36130  midofsegid  36562  outsideofeq  36588  hfun  36636  ordcmp  36924  icoreclin  37969  itgabsnc  38306  dvasin  38321  cvrat  40164  4atlem10  40348  4atlem12  40354  cdleme18d  41037  cdleme22b  41083  cdleme32e  41187  lclkrlem2e  42253  aks4d1p1  42811  pell1234qrdich  43558  onsupnmax  43925  omlimcl2  43939  onexlimgt  43940  onexoegt  43941  onsucf1olem  43967  oege1  44003  cantnfresb  44021  omabs2  44029  tfsconcat0b  44043  clsk1indlem3  44739  suctrALT  45504  wallispilem3  46751  nprmmul2  48244  bgoldbtbnd  48541  reorelicc  49457  infsubc  49805  infsubc2  49806