Theorem mpjaod 876

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

Syntax hints:   → wi 4   ∨ wo 863

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 198  df-or 864

This theorem is referenced by:  ecase2d  1043  opth1  5085  sorpssun  7112  sorpssin  7113  reldmtpos  7533  dftpos4  7544  oaass  7816  nnawordex  7892  omabs  7902  suplub2  8544  en3lplem2  8693  cantnflt  8754  cantnfp1lem3  8762  tcrank  8932  cardaleph  9133  fpwwe2  9688  gchpwdom  9715  grur1  9865  indpi  9952  nn1suc  11264  nnsub  11282  seqid  13075  seqz  13078  faclbnd  13303  facavg  13314  bcval5  13331  hashnnn0genn0  13357  hashfzo  13440  sqrlem6  14218  resqrex  14221  absmod0  14273  absz  14281  iserex  14617  fsumf1o  14684  fsumss  14686  fsumcl2lem  14692  fsumadd  14700  fsummulc2  14745  fsumconst  14751  fsumrelem  14768  isumsplit  14801  fprodf1o  14905  fprodss  14907  fprodcl2lem  14909  fprodmul  14919  fproddiv  14920  fprodconst  14937  fprodn0  14938  absdvdsb  15231  dvdsabsb  15232  gcdabs1  15480  bezoutlem1  15485  bezoutlem2  15486  isprm5  15646  pcabs  15806  pockthg  15837  prmreclem5  15851  vdwlem13  15924  0ram  15951  ram0  15953  prmlem0  16039  mulgnn0ass  17806  psgnunilem2  18142  mndodcongi  18189  oddvdsnn0  18190  odnncl  18191  efgredlemb  18386  gsumzres  18537  gsumzcl2  18538  gsumzf1o  18540  gsumzaddlem  18548  gsumconst  18561  gsumzmhm  18564  gsummulglem  18568  gsumzoppg  18571  pgpfac1lem5  18706  mplsubrglem  19674  gsumfsum  20048  zringlpirlem1  20067  ordthaus  21429  icccmplem2  22866  metdstri  22894  ioombl  23573  itgabs  23842  dvlip  23997  dvge0  24010  dvivthlem1  24012  dvcnvrelem1  24021  ply1rem  24164  dgrcolem2  24271  quotcan  24305  sinq12ge0  24502  argregt0  24598  argrege0  24599  scvxcvx  24954  bpos1lem  25249  bposlem3  25253  lgseisenlem2  25343  frgrregord013  27611  htthlem  28131  atcvati  29602  sinccvglem  31921  noextendseq  32174  noetalem3  32219  midofsegid  32565  outsideofeq  32591  hfun  32639  ordcmp  32800  icoreclin  33559  itgabsnc  33828  dvasin  33845  cvrat  35246  4atlem10  35430  4atlem12  35436  cdleme18d  36120  cdleme22b  36166  cdleme32e  36270  lclkrlem2e  37336  pell1234qrdich  37966  clsk1indlem3  38881  suctrALT  39595  wallispilem3  40807  bgoldbtbnd  42249