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

This theorem is referenced by:  ecase2d  978  opth1  4870  sorpssun  6842  sorpssin  6843  reldmtpos  7247  dftpos4  7258  oaass  7528  nnawordex  7604  omabs  7614  suplub2  8250  en3lplem2  8395  cantnflt  8452  cantnfp1lem3  8460  tcrank  8630  cardaleph  8795  fpwwe2  9344  gchpwdom  9371  grur1  9521  indpi  9608  nn1suc  10918  nnsub  10936  seqid  12708  seqz  12711  faclbnd  12939  facavg  12950  bcval5  12967  hashnnn0genn0  12993  hashfzo  13076  sqrlem6  13836  resqrex  13839  absmod0  13891  absz  13899  iserex  14235  fsumf1o  14301  fsumss  14303  fsumcl2lem  14309  fsumadd  14317  fsummulc2  14358  fsumconst  14364  fsumrelem  14380  isumsplit  14411  fprodf1o  14515  fprodss  14517  fprodcl2lem  14519  fprodmul  14529  fproddiv  14530  fprodconst  14547  fprodn0  14548  absdvdsb  14838  dvdsabsb  14839  gcdabs1  15089  bezoutlem1  15094  bezoutlem2  15095  isprm5  15257  pcabs  15417  pockthg  15448  prmreclem5  15462  vdwlem13  15535  0ram  15562  ram0  15564  prmlem0  15650  mulgnn0ass  17401  psgnunilem2  17738  mndodcongi  17785  oddvdsnn0  17786  odnncl  17787  efgredlemb  17982  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumconst  18157  gsumzmhm  18160  gsummulglem  18164  gsumzoppg  18167  pgpfac1lem5  18301  mplsubrglem  19260  gsumfsum  19632  zringlpirlem1  19651  ordthaus  20998  icccmplem2  22434  metdstri  22462  ioombl  23140  itgabs  23407  dvlip  23560  dvge0  23573  dvivthlem1  23575  dvcnvrelem1  23584  ply1rem  23727  dgrcolem2  23834  quotcan  23868  sinq12ge0  24064  argregt0  24160  argrege0  24161  scvxcvx  24512  bpos1lem  24807  bposlem3  24811  lgseisenlem2  24901  frgraregord013  26645  htthlem  27158  atcvati  28629  sinccvglem  30820  midofsegid  31381  outsideofeq  31407  hfun  31455  ordcmp  31616  icoreclin  32381  itgabsnc  32649  dvasin  32666  cvrat  33726  4atlem10  33910  4atlem12  33916  cdleme18d  34600  cdleme22b  34647  cdleme32e  34751  lclkrlem2e  35818  pell1234qrdich  36443  clsk1indlem3  37361  suctrALT  38083  wallispilem3  38960  bgoldbtbnd  40225  av-frgraregord013  41549