Theorem mpjaod 857

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

Syntax hints:   → wi 4   ∨ wo 844

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 845

This theorem is referenced by:  ecase2dOLD  1028  opth1  5391  onun2  6374  sorpssun  7592  sorpssin  7593  reldmtpos  8059  dftpos4  8070  oaass  8401  nnawordex  8477  omabs  8490  suplub2  9229  en3lplem2  9380  cantnflt  9439  cantnfp1lem3  9447  ttrclselem2  9493  tcrank  9651  cardaleph  9854  fpwwe2  10408  gchpwdom  10435  grur1  10585  indpi  10672  nn1suc  12004  nnsub  12026  seqid  13777  seqz  13780  faclbnd  14013  facavg  14024  bcval5  14041  hashnnn0genn0  14066  hashfzo  14153  sqrlem6  14968  resqrex  14971  absmod0  15024  absz  15032  iserex  15377  fsumf1o  15444  fsumss  15446  fsumcl2lem  15452  fsumadd  15461  fsummulc2  15505  fsumconst  15511  fsumrelem  15528  isumsplit  15561  fprodf1o  15665  fprodss  15667  fprodcl2lem  15669  fprodmul  15679  fproddiv  15680  fprodconst  15697  fprodn0  15698  absdvdsb  15993  dvdsabsb  15994  gcdabs1  16245  bezoutlem1  16256  bezoutlem2  16257  2mulprm  16407  isprm5  16421  pcabs  16585  pockthg  16616  prmreclem5  16630  vdwlem13  16703  0ram  16730  ram0  16732  prmlem0  16816  mulgnn0ass  18748  psgnunilem2  19112  mndodcongi  19160  oddvdsnn0  19161  odnncl  19162  efgredlemb  19361  gsumzres  19519  gsumzcl2  19520  gsumzf1o  19522  gsumzaddlem  19531  gsumconst  19544  gsumzmhm  19547  gsummulglem  19551  gsumzoppg  19554  pgpfac1lem5  19691  ablsimpnosubgd  19716  gsumfsum  20674  zringlpirlem1  20693  mplsubrglem  21219  ordthaus  22544  icccmplem2  23995  metdstri  24023  ioombl  24738  itgabs  25008  dvlip  25166  dvge0  25179  dvivthlem1  25181  dvcnvrelem1  25190  ply1rem  25337  dgrcolem2  25444  quotcan  25478  sinq12ge0  25674  argregt0  25774  argrege0  25775  scvxcvx  26144  bpos1lem  26439  bposlem3  26443  lgseisenlem2  26533  frgrregord013  28768  htthlem  29288  atcvati  30757  ccatf1  31232  sinccvglem  33639  poxp2  33799  poxp3  33805  noextendseq  33879  nogt01o  33908  nosupprefixmo  33912  noinfprefixmo  33913  noinfbnd1lem5  33939  noetasuplem4  33948  noetainflem4  33952  midofsegid  34415  outsideofeq  34441  hfun  34489  ordcmp  34645  icoreclin  35537  itgabsnc  35855  dvasin  35870  cvrat  37443  4atlem10  37627  4atlem12  37633  cdleme18d  38316  cdleme22b  38362  cdleme32e  38466  lclkrlem2e  39532  aks4d1p1  40091  pell1234qrdich  40690  clsk1indlem3  41660  suctrALT  42453  wallispilem3  43615  bgoldbtbnd  45272  reorelicc  46067