Theorem mpjaod 860

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

Syntax hints:   → wi 4   ∨ wo 847

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 210  df-or 848

This theorem is referenced by:  ecase2dOLD  1031  opth1  5359  onun2  6317  sorpssun  7518  sorpssin  7519  reldmtpos  7976  dftpos4  7987  oaass  8289  nnawordex  8365  omabs  8376  suplub2  9077  en3lplem2  9228  cantnflt  9287  cantnfp1lem3  9295  tcrank  9500  cardaleph  9703  fpwwe2  10257  gchpwdom  10284  grur1  10434  indpi  10521  nn1suc  11852  nnsub  11874  seqid  13621  seqz  13624  faclbnd  13856  facavg  13867  bcval5  13884  hashnnn0genn0  13909  hashfzo  13996  sqrlem6  14811  resqrex  14814  absmod0  14867  absz  14875  iserex  15220  fsumf1o  15287  fsumss  15289  fsumcl2lem  15295  fsumadd  15304  fsummulc2  15348  fsumconst  15354  fsumrelem  15371  isumsplit  15404  fprodf1o  15508  fprodss  15510  fprodcl2lem  15512  fprodmul  15522  fproddiv  15523  fprodconst  15540  fprodn0  15541  absdvdsb  15836  dvdsabsb  15837  gcdabs1  16088  bezoutlem1  16099  bezoutlem2  16100  2mulprm  16250  isprm5  16264  pcabs  16428  pockthg  16459  prmreclem5  16473  vdwlem13  16546  0ram  16573  ram0  16575  prmlem0  16659  mulgnn0ass  18527  psgnunilem2  18887  mndodcongi  18935  oddvdsnn0  18936  odnncl  18937  efgredlemb  19136  gsumzres  19294  gsumzcl2  19295  gsumzf1o  19297  gsumzaddlem  19306  gsumconst  19319  gsumzmhm  19322  gsummulglem  19326  gsumzoppg  19329  pgpfac1lem5  19466  ablsimpnosubgd  19491  gsumfsum  20430  zringlpirlem1  20449  mplsubrglem  20966  ordthaus  22281  icccmplem2  23720  metdstri  23748  ioombl  24462  itgabs  24732  dvlip  24890  dvge0  24903  dvivthlem1  24905  dvcnvrelem1  24914  ply1rem  25061  dgrcolem2  25168  quotcan  25202  sinq12ge0  25398  argregt0  25498  argrege0  25499  scvxcvx  25868  bpos1lem  26163  bposlem3  26167  lgseisenlem2  26257  frgrregord013  28478  htthlem  28998  atcvati  30467  ccatf1  30943  sinccvglem  33343  poxp2  33527  poxp3  33533  noextendseq  33607  nogt01o  33636  nosupprefixmo  33640  noinfprefixmo  33641  noinfbnd1lem5  33667  noetasuplem4  33676  noetainflem4  33680  midofsegid  34143  outsideofeq  34169  hfun  34217  ordcmp  34373  icoreclin  35265  itgabsnc  35583  dvasin  35598  cvrat  37173  4atlem10  37357  4atlem12  37363  cdleme18d  38046  cdleme22b  38092  cdleme32e  38196  lclkrlem2e  39262  aks4d1p1  39817  pell1234qrdich  40386  clsk1indlem3  41330  suctrALT  42119  wallispilem3  43283  bgoldbtbnd  44934  reorelicc  45729