Theorem mpjaod 861

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

Syntax hints:   → wi 4   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  opth1  5429  onun2  6434  sorpssun  7684  sorpssin  7685  omun  7839  poxp2  8093  poxp3  8100  reldmtpos  8184  dftpos4  8195  oaass  8496  nnawordex  8573  omabs  8587  suplub2  9374  en3lplem2  9534  cantnflt  9593  cantnfp1lem3  9601  ttrclselem2  9647  tcrank  9808  cardaleph  10011  fpwwe2  10566  gchpwdom  10593  grur1  10743  indpi  10830  nn1suc  12196  nnsub  12221  seqid  14009  seqz  14012  faclbnd  14252  facavg  14263  bcval5  14280  hashnnn0genn0  14305  hashfzo  14391  01sqrexlem6  15209  resqrex  15212  absmod0  15265  absz  15273  iserex  15619  fsumf1o  15685  fsumss  15687  fsumcl2lem  15693  fsumadd  15702  fsummulc2  15746  fsumconst  15752  fsumrelem  15770  isumsplit  15805  fprodf1o  15911  fprodss  15913  fprodcl2lem  15915  fprodmul  15925  fproddiv  15926  fprodconst  15943  fprodn0  15944  absdvdsb  16243  dvdsabsb  16244  gcdabs1  16498  bezoutlem1  16508  bezoutlem2  16509  2mulprm  16662  isprm5  16677  pcabs  16846  pockthg  16877  prmreclem5  16891  vdwlem13  16964  0ram  16991  ram0  16993  prmlem0  17076  mulgnn0ass  19086  psgnunilem2  19470  mndodcongi  19518  oddvdsnn0  19519  odnncl  19520  efgredlemb  19721  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumzaddlem  19896  gsumconst  19909  gsumzmhm  19912  gsummulglem  19916  gsumzoppg  19919  pgpfac1lem5  20056  ablsimpnosubgd  20081  gsumfsum  21414  zringlpirlem1  21442  mplsubrglem  21982  ordthaus  23349  icccmplem2  24789  metdstri  24817  ioombl  25532  itgabs  25802  dvlip  25960  dvge0  25973  dvivthlem1  25975  dvcnvrelem1  25984  ply1rem  26131  dgrcolem2  26239  quotcan  26275  sinq12ge0  26472  argregt0  26574  argrege0  26575  scvxcvx  26949  bpos1lem  27245  bposlem3  27249  lgseisenlem2  27339  noextendseq  27631  nogt01o  27660  nosupprefixmo  27664  noinfprefixmo  27665  noinfbnd1lem5  27691  noetasuplem4  27700  noetainflem4  27704  n0subs  28355  bdayfinbndlem1  28459  bdayfinlem  28478  bdayfin  28479  frgrregord013  30465  htthlem  30988  atcvati  32457  ccatf1  33009  sinccvglem  35854  midofsegid  36286  outsideofeq  36312  hfun  36360  ordcmp  36629  icoreclin  37673  itgabsnc  38010  dvasin  38025  cvrat  39868  4atlem10  40052  4atlem12  40058  cdleme18d  40741  cdleme22b  40787  cdleme32e  40891  lclkrlem2e  41957  aks4d1p1  42515  pell1234qrdich  43289  onsupnmax  43656  omlimcl2  43670  onexlimgt  43671  onexoegt  43672  onsucf1olem  43698  oege1  43734  cantnfresb  43752  omabs2  43760  tfsconcat0b  43774  clsk1indlem3  44470  suctrALT  45252  wallispilem3  46495  nprmmul2  47982  bgoldbtbnd  48279  reorelicc  49180  infsubc  49529  infsubc2  49530