Theorem mpjaod 855

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

Syntax hints:   → wi 4   ∨ wo 842

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 208  df-or 843

This theorem is referenced by:  ecase2d  1024  opth1  5266  sorpssun  7321  sorpssin  7322  reldmtpos  7758  dftpos4  7769  oaass  8044  nnawordex  8120  omabs  8131  suplub2  8778  en3lplem2  8929  cantnflt  8988  cantnfp1lem3  8996  tcrank  9166  cardaleph  9368  fpwwe2  9918  gchpwdom  9945  grur1  10095  indpi  10182  nn1suc  11513  nnsub  11535  seqid  13269  seqz  13272  faclbnd  13504  facavg  13515  bcval5  13532  hashnnn0genn0  13557  hashfzo  13642  sqrlem6  14445  resqrex  14448  absmod0  14501  absz  14509  iserex  14851  fsumf1o  14917  fsumss  14919  fsumcl2lem  14925  fsumadd  14933  fsummulc2  14976  fsumconst  14982  fsumrelem  14999  isumsplit  15032  fprodf1o  15137  fprodss  15139  fprodcl2lem  15141  fprodmul  15151  fproddiv  15152  fprodconst  15169  fprodn0  15170  absdvdsb  15465  dvdsabsb  15466  gcdabs1  15715  bezoutlem1  15720  bezoutlem2  15721  2mulprm  15870  isprm5  15884  pcabs  16044  pockthg  16075  prmreclem5  16089  vdwlem13  16162  0ram  16189  ram0  16191  prmlem0  16272  mulgnn0ass  18021  psgnunilem2  18358  mndodcongi  18406  oddvdsnn0  18407  odnncl  18408  efgredlemb  18603  gsumzres  18754  gsumzcl2  18755  gsumzf1o  18757  gsumzaddlem  18765  gsumconst  18778  gsumzmhm  18781  gsummulglem  18785  gsumzoppg  18788  pgpfac1lem5  18922  mplsubrglem  19911  gsumfsum  20298  zringlpirlem1  20317  ordthaus  21680  icccmplem2  23118  metdstri  23146  ioombl  23853  itgabs  24122  dvlip  24277  dvge0  24290  dvivthlem1  24292  dvcnvrelem1  24301  ply1rem  24444  dgrcolem2  24551  quotcan  24585  sinq12ge0  24781  argregt0  24878  argrege0  24879  scvxcvx  25249  bpos1lem  25544  bposlem3  25548  lgseisenlem2  25638  frgrregord013  27862  htthlem  28381  atcvati  29850  sinccvglem  32525  noextendseq  32785  noetalem3  32830  midofsegid  33176  outsideofeq  33202  hfun  33250  ordcmp  33406  icoreclin  34190  itgabsnc  34513  dvasin  34530  cvrat  36110  4atlem10  36294  4atlem12  36300  cdleme18d  36983  cdleme22b  37029  cdleme32e  37133  lclkrlem2e  38199  pell1234qrdich  38964  clsk1indlem3  39899  ablsimpnosubgd  40183  suctrALT  40720  wallispilem3  41916  bgoldbtbnd  43478  reorelicc  44200