Theorem mpjaod 859

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

Syntax hints:   → wi 4   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  ecase2dOLD  1030  opth1  5475  onun2  6470  sorpssun  7717  sorpssin  7718  omun  7875  poxp2  8126  poxp3  8133  reldmtpos  8216  dftpos4  8227  oaass  8558  nnawordex  8634  omabs  8647  suplub2  9453  en3lplem2  9605  cantnflt  9664  cantnfp1lem3  9672  ttrclselem2  9718  tcrank  9876  cardaleph  10081  fpwwe2  10635  gchpwdom  10662  grur1  10812  indpi  10899  nn1suc  12231  nnsub  12253  seqid  14010  seqz  14013  faclbnd  14247  facavg  14258  bcval5  14275  hashnnn0genn0  14300  hashfzo  14386  01sqrexlem6  15191  resqrex  15194  absmod0  15247  absz  15255  iserex  15600  fsumf1o  15666  fsumss  15668  fsumcl2lem  15674  fsumadd  15683  fsummulc2  15727  fsumconst  15733  fsumrelem  15750  isumsplit  15783  fprodf1o  15887  fprodss  15889  fprodcl2lem  15891  fprodmul  15901  fproddiv  15902  fprodconst  15919  fprodn0  15920  absdvdsb  16215  dvdsabsb  16216  gcdabs1  16467  bezoutlem1  16478  bezoutlem2  16479  2mulprm  16627  isprm5  16641  pcabs  16805  pockthg  16836  prmreclem5  16850  vdwlem13  16923  0ram  16950  ram0  16952  prmlem0  17036  mulgnn0ass  18985  psgnunilem2  19358  mndodcongi  19406  oddvdsnn0  19407  odnncl  19408  efgredlemb  19609  gsumzres  19772  gsumzcl2  19773  gsumzf1o  19775  gsumzaddlem  19784  gsumconst  19797  gsumzmhm  19800  gsummulglem  19804  gsumzoppg  19807  pgpfac1lem5  19944  ablsimpnosubgd  19969  gsumfsum  21005  zringlpirlem1  21024  mplsubrglem  21555  ordthaus  22880  icccmplem2  24331  metdstri  24359  ioombl  25074  itgabs  25344  dvlip  25502  dvge0  25515  dvivthlem1  25517  dvcnvrelem1  25526  ply1rem  25673  dgrcolem2  25780  quotcan  25814  sinq12ge0  26010  argregt0  26110  argrege0  26111  scvxcvx  26480  bpos1lem  26775  bposlem3  26779  lgseisenlem2  26869  noextendseq  27160  nogt01o  27189  nosupprefixmo  27193  noinfprefixmo  27194  noinfbnd1lem5  27220  noetasuplem4  27229  noetainflem4  27233  frgrregord013  29638  htthlem  30158  atcvati  31627  ccatf1  32103  sinccvglem  34646  midofsegid  35065  outsideofeq  35091  hfun  35139  ordcmp  35321  icoreclin  36227  itgabsnc  36546  dvasin  36561  cvrat  38282  4atlem10  38466  4atlem12  38472  cdleme18d  39155  cdleme22b  39201  cdleme32e  39305  lclkrlem2e  40371  aks4d1p1  40930  pell1234qrdich  41585  onsupnmax  41963  omlimcl2  41977  onexlimgt  41978  onexoegt  41979  onsucf1olem  42006  oege1  42042  cantnfresb  42060  omabs2  42068  tfsconcat0b  42082  clsk1indlem3  42780  suctrALT  43573  wallispilem3  44770  bgoldbtbnd  46464  reorelicc  47350