Theorem mpjaod 874

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

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

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 862

This theorem is used by:  opth1  5443  onun2  6473  sorpssun  7746  sorpssin  7747  omun  7899  poxp2  8160  poxp3  8167  reldmtpos  8252  dftpos4  8263  oaass  8570  nnawordex  8647  omabs  8661  suplub2  9454  en3lplem2  9615  cantnflt  9674  cantnfp1lem3  9682  ttrclselem2  9728  tcrank  9902  hfunOLD  9920  cardaleph  10169  fpwwe2  10729  gchpwdom  10756  grur1  10906  indpi  10993  nn1suc  12358  nnsub  12383  seqid  14191  seqz  14194  faclbnd  14435  facavg  14446  bcval5  14463  hashnnn0genn0  14488  hashfzo  14575  ccatf1  14737  01sqrexlem6  15415  resqrex  15418  absmod0  15471  absz  15479  iserex  15825  fsumf1o  15890  fsumss  15892  fsumcl2lem  15898  fsumadd  15907  fsummulc2  15951  fsumconst  15957  fsumrelem  15975  isumsplit  16010  fprodf1o  16114  fprodss  16116  fprodcl2lem  16118  fprodmul  16128  fproddiv  16129  fprodconst  16146  fprodn0  16147  absdvdsb  16445  dvdsabsb  16446  gcdabs1  16703  bezoutlem1  16713  bezoutlem2  16714  2mulprm  16869  isprm5  16884  pcabs  17054  pockthg  17085  prmreclem5  17099  vdwlem13  17172  0ram  17199  ram0  17201  prmlem0  17284  mulgnn0ass  19321  psgnunilem2  19710  mndodcongi  19758  oddvdsnn0  19759  odnncl  19760  efgredlemb  19961  gsumzres  20124  gsumzcl2  20125  gsumzf1o  20127  gsumzaddlem  20136  gsumconst  20149  gsumzmhm  20152  gsummulglem  20156  gsumzoppg  20159  pgpfac1lem5  20296  ablsimpnosubgd  20321  gsumfsum  21741  zringlpirlem1  21769  mplsubrglem  22312  ordthaus  23703  icccmplem2  25144  metdstri  25172  ioombl  25887  itgabs  26156  dvlip  26314  dvge0  26327  dvivthlem1  26329  dvcnvrelem1  26338  ply1rem  26485  dgrcolem2  26594  quotcan  26633  sinq12ge0  26838  argregt0  26939  argrege0  26940  scvxcvx  27314  bpos1lem  27610  bposlem3  27614  lgseisenlem2  27704  fltoprm  27996  noextendseq  28025  nogt01o  28054  nosupprefixmo  28058  noinfprefixmo  28059  noinfbnd1lem5  28085  noetasuplem4  28094  noetainflem4  28098  n0subs  28750  bdayfinbndlem1  28854  bdayfinlem  28873  bdayfin  28874  frgrregord013  30997  htthlem  31520  atcvati  32989  maxssj0  35938  sinccvglem  36506  mirimanoffr  36529  midofsegid  36944  outsideofeq  36970  ordcmp  37310  icoreclin  38356  itgabsnc  38683  dvasin  38698  cvrat  40555  4atlem10  40739  4atlem12  40745  cdleme18d  41428  cdleme22b  41474  cdleme32e  41578  lclkrlem2e  42644  aks4d1p1  43202  pell1234qrdich  43944  onsupnmax  44306  omlimcl2  44320  onexlimgt  44321  onexoegt  44322  onsucf1olem  44348  oege1  44384  cantnfresb  44402  omabs2  44410  tfsconcat0b  44424  clsk1indlem3  45119  suctrALT  45884  wallispilem3  47153  nprmmul2  48686  bgoldbtbnd  48983  reorelicc  49898  infsubc  50244  infsubc2  50245