Theorem mpjaod 856

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

Syntax hints:   → wi 4   ∨ wo 843

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 844

This theorem is referenced by:  ecase2dOLD  1027  opth1  5384  onun2  6355  sorpssun  7561  sorpssin  7562  reldmtpos  8021  dftpos4  8032  oaass  8354  nnawordex  8430  omabs  8441  suplub2  9150  en3lplem2  9301  cantnflt  9360  cantnfp1lem3  9368  tcrank  9573  cardaleph  9776  fpwwe2  10330  gchpwdom  10357  grur1  10507  indpi  10594  nn1suc  11925  nnsub  11947  seqid  13696  seqz  13699  faclbnd  13932  facavg  13943  bcval5  13960  hashnnn0genn0  13985  hashfzo  14072  sqrlem6  14887  resqrex  14890  absmod0  14943  absz  14951  iserex  15296  fsumf1o  15363  fsumss  15365  fsumcl2lem  15371  fsumadd  15380  fsummulc2  15424  fsumconst  15430  fsumrelem  15447  isumsplit  15480  fprodf1o  15584  fprodss  15586  fprodcl2lem  15588  fprodmul  15598  fproddiv  15599  fprodconst  15616  fprodn0  15617  absdvdsb  15912  dvdsabsb  15913  gcdabs1  16164  bezoutlem1  16175  bezoutlem2  16176  2mulprm  16326  isprm5  16340  pcabs  16504  pockthg  16535  prmreclem5  16549  vdwlem13  16622  0ram  16649  ram0  16651  prmlem0  16735  mulgnn0ass  18654  psgnunilem2  19018  mndodcongi  19066  oddvdsnn0  19067  odnncl  19068  efgredlemb  19267  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumzaddlem  19437  gsumconst  19450  gsumzmhm  19453  gsummulglem  19457  gsumzoppg  19460  pgpfac1lem5  19597  ablsimpnosubgd  19622  gsumfsum  20577  zringlpirlem1  20596  mplsubrglem  21120  ordthaus  22443  icccmplem2  23892  metdstri  23920  ioombl  24634  itgabs  24904  dvlip  25062  dvge0  25075  dvivthlem1  25077  dvcnvrelem1  25086  ply1rem  25233  dgrcolem2  25340  quotcan  25374  sinq12ge0  25570  argregt0  25670  argrege0  25671  scvxcvx  26040  bpos1lem  26335  bposlem3  26339  lgseisenlem2  26429  frgrregord013  28660  htthlem  29180  atcvati  30649  ccatf1  31125  sinccvglem  33530  ttrclselem2  33712  poxp2  33717  poxp3  33723  noextendseq  33797  nogt01o  33826  nosupprefixmo  33830  noinfprefixmo  33831  noinfbnd1lem5  33857  noetasuplem4  33866  noetainflem4  33870  midofsegid  34333  outsideofeq  34359  hfun  34407  ordcmp  34563  icoreclin  35455  itgabsnc  35773  dvasin  35788  cvrat  37363  4atlem10  37547  4atlem12  37553  cdleme18d  38236  cdleme22b  38282  cdleme32e  38386  lclkrlem2e  39452  aks4d1p1  40012  pell1234qrdich  40599  clsk1indlem3  41542  suctrALT  42335  wallispilem3  43498  bgoldbtbnd  45149  reorelicc  45944