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  5448  onun2  6460  sorpssun  7717  sorpssin  7718  omun  7872  poxp2  8127  poxp3  8134  reldmtpos  8218  dftpos4  8229  oaass  8534  nnawordex  8611  omabs  8625  suplub2  9409  en3lplem2  9570  cantnflt  9629  cantnfp1lem3  9637  ttrclselem2  9683  tcrank  9844  cardaleph  10061  fpwwe2  10616  gchpwdom  10643  grur1  10793  indpi  10880  nn1suc  12246  nnsub  12271  seqid  14074  seqz  14077  faclbnd  14317  facavg  14328  bcval5  14345  hashnnn0genn0  14370  hashfzo  14456  01sqrexlem6  15288  resqrex  15291  absmod0  15344  absz  15352  iserex  15698  fsumf1o  15764  fsumss  15766  fsumcl2lem  15772  fsumadd  15781  fsummulc2  15825  fsumconst  15831  fsumrelem  15849  isumsplit  15884  fprodf1o  15990  fprodss  15992  fprodcl2lem  15994  fprodmul  16004  fproddiv  16005  fprodconst  16022  fprodn0  16023  absdvdsb  16322  dvdsabsb  16323  gcdabs1  16577  bezoutlem1  16587  bezoutlem2  16588  2mulprm  16741  isprm5  16756  pcabs  16925  pockthg  16956  prmreclem5  16970  vdwlem13  17043  0ram  17070  ram0  17072  prmlem0  17155  mulgnn0ass  19167  psgnunilem2  19556  mndodcongi  19604  oddvdsnn0  19605  odnncl  19606  efgredlemb  19807  gsumzres  19970  gsumzcl2  19971  gsumzf1o  19973  gsumzaddlem  19982  gsumconst  19995  gsumzmhm  19998  gsummulglem  20002  gsumzoppg  20005  pgpfac1lem5  20142  ablsimpnosubgd  20167  gsumfsum  21544  zringlpirlem1  21572  mplsubrglem  22113  ordthaus  23502  icccmplem2  24942  metdstri  24970  ioombl  25685  itgabs  25955  dvlip  26113  dvge0  26126  dvivthlem1  26128  dvcnvrelem1  26137  ply1rem  26284  dgrcolem2  26392  quotcan  26431  sinq12ge0  26631  argregt0  26733  argrege0  26734  scvxcvx  27108  bpos1lem  27404  bposlem3  27408  lgseisenlem2  27498  noextendseq  27789  nogt01o  27818  nosupprefixmo  27822  noinfprefixmo  27823  noinfbnd1lem5  27849  noetasuplem4  27858  noetainflem4  27862  n0subs  28514  bdayfinbndlem1  28618  bdayfinlem  28637  bdayfin  28638  frgrregord013  30655  htthlem  31178  atcvati  32647  ccatf1  33182  sinccvglem  36035  midofsegid  36467  outsideofeq  36493  hfun  36541  ordcmp  36820  icoreclin  37863  itgabsnc  38200  dvasin  38215  cvrat  40058  4atlem10  40242  4atlem12  40248  cdleme18d  40931  cdleme22b  40977  cdleme32e  41081  lclkrlem2e  42147  aks4d1p1  42705  pell1234qrdich  43450  onsupnmax  43817  omlimcl2  43831  onexlimgt  43832  onexoegt  43833  onsucf1olem  43859  oege1  43895  cantnfresb  43913  omabs2  43921  tfsconcat0b  43935  clsk1indlem3  44631  suctrALT  45399  wallispilem3  46639  nprmmul2  48132  bgoldbtbnd  48429  reorelicc  49341  infsubc  49689  infsubc2  49690