Theorem mpjaod 395

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

Syntax hints:   → wi 4   ∨ wo 382

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 197  df-or 384

This theorem is referenced by:  ecase2d  1000  opth1  4973  sorpssun  6986  sorpssin  6987  reldmtpos  7405  dftpos4  7416  oaass  7686  nnawordex  7762  omabs  7772  suplub2  8408  en3lplem2  8550  cantnflt  8607  cantnfp1lem3  8615  tcrank  8785  cardaleph  8950  fpwwe2  9503  gchpwdom  9530  grur1  9680  indpi  9767  nn1suc  11079  nnsub  11097  seqid  12886  seqz  12889  faclbnd  13117  facavg  13128  bcval5  13145  hashnnn0genn0  13171  hashfzo  13254  sqrlem6  14032  resqrex  14035  absmod0  14087  absz  14095  iserex  14431  fsumf1o  14498  fsumss  14500  fsumcl2lem  14506  fsumadd  14514  fsummulc2  14560  fsumconst  14566  fsumrelem  14583  isumsplit  14616  fprodf1o  14720  fprodss  14722  fprodcl2lem  14724  fprodmul  14734  fproddiv  14735  fprodconst  14752  fprodn0  14753  absdvdsb  15047  dvdsabsb  15048  gcdabs1  15298  bezoutlem1  15303  bezoutlem2  15304  isprm5  15466  pcabs  15626  pockthg  15657  prmreclem5  15671  vdwlem13  15744  0ram  15771  ram0  15773  prmlem0  15859  mulgnn0ass  17625  psgnunilem2  17961  mndodcongi  18008  oddvdsnn0  18009  odnncl  18010  efgredlemb  18205  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumconst  18380  gsumzmhm  18383  gsummulglem  18387  gsumzoppg  18390  pgpfac1lem5  18524  mplsubrglem  19487  gsumfsum  19861  zringlpirlem1  19880  ordthaus  21236  icccmplem2  22673  metdstri  22701  ioombl  23379  itgabs  23646  dvlip  23801  dvge0  23814  dvivthlem1  23816  dvcnvrelem1  23825  ply1rem  23968  dgrcolem2  24075  quotcan  24109  sinq12ge0  24305  argregt0  24401  argrege0  24402  scvxcvx  24757  bpos1lem  25052  bposlem3  25056  lgseisenlem2  25146  frgrregord013  27382  htthlem  27902  atcvati  29373  sinccvglem  31692  noextendseq  31945  noetalem3  31990  midofsegid  32336  outsideofeq  32362  hfun  32410  ordcmp  32571  icoreclin  33335  itgabsnc  33609  dvasin  33626  cvrat  35026  4atlem10  35210  4atlem12  35216  cdleme18d  35900  cdleme22b  35946  cdleme32e  36050  lclkrlem2e  37117  pell1234qrdich  37742  clsk1indlem3  38658  suctrALT  39375  wallispilem3  40602  bgoldbtbnd  42022