Theorem mpjaod 856

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

Syntax hints:   → wi 4   ∨ wo 843

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 844

This theorem is referenced by:  ecase2d  1026  opth1  5367  sorpssun  7456  sorpssin  7457  reldmtpos  7900  dftpos4  7911  oaass  8187  nnawordex  8263  omabs  8274  suplub2  8925  en3lplem2  9076  cantnflt  9135  cantnfp1lem3  9143  tcrank  9313  cardaleph  9515  fpwwe2  10065  gchpwdom  10092  grur1  10242  indpi  10329  nn1suc  11660  nnsub  11682  seqid  13416  seqz  13419  faclbnd  13651  facavg  13662  bcval5  13679  hashnnn0genn0  13704  hashfzo  13791  sqrlem6  14607  resqrex  14610  absmod0  14663  absz  14671  iserex  15013  fsumf1o  15080  fsumss  15082  fsumcl2lem  15088  fsumadd  15096  fsummulc2  15139  fsumconst  15145  fsumrelem  15162  isumsplit  15195  fprodf1o  15300  fprodss  15302  fprodcl2lem  15304  fprodmul  15314  fproddiv  15315  fprodconst  15332  fprodn0  15333  absdvdsb  15628  dvdsabsb  15629  gcdabs1  15878  bezoutlem1  15887  bezoutlem2  15888  2mulprm  16037  isprm5  16051  pcabs  16211  pockthg  16242  prmreclem5  16256  vdwlem13  16329  0ram  16356  ram0  16358  prmlem0  16439  mulgnn0ass  18263  psgnunilem2  18623  mndodcongi  18671  oddvdsnn0  18672  odnncl  18673  efgredlemb  18872  gsumzres  19029  gsumzcl2  19030  gsumzf1o  19032  gsumzaddlem  19041  gsumconst  19054  gsumzmhm  19057  gsummulglem  19061  gsumzoppg  19064  pgpfac1lem5  19201  ablsimpnosubgd  19226  mplsubrglem  20219  gsumfsum  20612  zringlpirlem1  20631  ordthaus  21992  icccmplem2  23431  metdstri  23459  ioombl  24166  itgabs  24435  dvlip  24590  dvge0  24603  dvivthlem1  24605  dvcnvrelem1  24614  ply1rem  24757  dgrcolem2  24864  quotcan  24898  sinq12ge0  25094  argregt0  25193  argrege0  25194  scvxcvx  25563  bpos1lem  25858  bposlem3  25862  lgseisenlem2  25952  frgrregord013  28174  htthlem  28694  atcvati  30163  ccatf1  30625  sinccvglem  32915  noextendseq  33174  noetalem3  33219  midofsegid  33565  outsideofeq  33591  hfun  33639  ordcmp  33795  icoreclin  34641  itgabsnc  34976  dvasin  34993  cvrat  36573  4atlem10  36757  4atlem12  36763  cdleme18d  37446  cdleme22b  37492  cdleme32e  37596  lclkrlem2e  38662  pell1234qrdich  39478  clsk1indlem3  40413  suctrALT  41180  wallispilem3  42372  bgoldbtbnd  43994  reorelicc  44717