Theorem mpjaodan 961

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30490. (Contributed by Mario Carneiro, 29-May-2016.)

Hypotheses

Ref	Expression
jaodan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
jaodan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)
jaodan.3	⊢ (𝜑 → (𝜓 ∨ 𝜃))

Assertion

Ref	Expression
mpjaodan	⊢ (𝜑 → 𝜒)

Proof of Theorem mpjaodan

Step	Hyp	Ref	Expression
1		jaodan.3	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃))
2		jaodan.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		jaodan.2	. . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	2, 3	jaodan 960	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
5	1, 4	mpdan 688	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848

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 207  df-an 396  df-or 849

This theorem is referenced by:  onunel  6432  weniso  7310  isf32lem2  10276  isf32lem4  10278  fpwwe2lem10  10563  fpwwe2lem11  10564  lecasei  11251  ltlecasei  11253  xaddass  13176  xlesubadd  13190  xmulge0  13211  xadddi2  13224  xrsupss  13236  xrinfmss  13237  fzm1  13535  seqf1olem2  13977  expaddzlem  14040  discr  14175  fzomaxdif  15279  iseralt  15620  sumrb  15648  telfsumo  15737  fsumparts  15741  ntrivcvgtail  15835  prodrb  15867  bitsf1  16385  smupvallem  16422  eucalgf  16522  eucalginv  16523  vdwmc2  16919  fvprif  17494  mreexmrid  17578  mreexexlem3d  17581  chnub  18557  chnccats1  18560  chnccat  18561  mulgfval  19011  ressmulgnn0  19019  mulgnn0p1  19027  mulgnn0subcl  19029  mulgsubcl  19030  mulgneg  19034  mulgz  19044  mulgnn0dir  19046  mulgdirlem  19047  mulgdir  19048  submmulg  19060  ghmmulg  19169  odid  19479  oddvds  19488  dfod2  19505  gexid  19522  gexdvds  19525  mulgnn0di  19766  mulgdi  19767  gsumzsplit  19868  2nsgsimpgd  20045  prmgrpsimpgd  20057  lringuplu  20489  lsppratlem5  21118  prmirred  21441  mhpmulcl  22104  1stckgenlem  23509  qtoprest  23673  tgpmulg  24049  tsmssplit  24108  xblss2ps  24357  xblss2  24358  metustfbas  24513  nmoix  24685  nmoleub  24687  idnghm  24699  blcvx  24754  icccmp  24782  xrge0tsms  24791  metdstri  24808  nmoleub2lem  25082  rrxcph  25360  rrxdstprj1  25377  ivthle  25425  ivthle2  25426  dyadmbl  25569  volivth  25576  itg2const2  25710  itg2mulc  25716  dvlip2  25968  dvfsumlem1  26000  mdegmullem  26051  coemulhi  26227  dgrcolem2  26248  coseq00topi  26479  abssinper  26498  cxplea  26673  cxple2  26674  cxple2a  26676  cxpcn3  26726  cxpaddlelem  26729  cxpaddle  26730  ang180lem3  26789  dcubic2  26822  birthdaylem2  26930  jensen  26967  ppiltx  27155  chtub  27191  bcmono  27256  bcmax  27257  bpos  27272  lgseisenlem1  27354  2sqlem4  27400  2sqmod  27415  pntrlog2bndlem5  27560  pntpbnd1  27565  noinfbnd2lem1  27710  noetasuplem4  27716  noetainflem4  27720  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  lemulsd  28146  mulsge0d  28154  mulscan2d  28187  lemuls1ad  28190  absmuls  28252  absnegs  28255  leabss  28256  tgldimor  28586  tgifscgr  28592  tgcgrxfr  28602  tgbtwnconn1  28659  tgbtwnconn2  28660  tgbtwnconn3  28661  tgbtwnconnln3  28662  tgbtwnconn22  28663  tgbtwnconnln1  28664  tgbtwnconnln2  28665  legtrid  28675  legbtwn  28678  tgcgrsub2  28679  legov3  28682  hlln  28691  hltr  28694  btwnhl  28698  ncolncol  28730  mirconn  28762  krippen  28775  midexlem  28776  midex  28821  opphllem2  28832  opphllem5  28835  opphllem6  28836  outpasch  28839  hlpasch  28840  trgcopyeulem  28889  cgrahl  28911  cgracol  28912  ex-natded5.7  30498  ex-natded5.13  30502  ex-natded9.20  30504  ex-natded9.20-2  30505  fconst7v  32709  suppovss  32770  nn0mnfxrd  32841  xrge0infss  32850  xnn0gt0  32859  nn0xmulclb  32861  difioo  32872  iundisjcnt  32888  f1ocnt  32890  fzo0opth  32893  hashxpe  32897  sgncl  32922  sgnmul  32926  nexple  32935  2exple2exp  32936  ccatws1f1o  33043  xrsmulgzz  33101  xrge0addgt0  33109  xrge0adddir  33110  ressmulgnn0d  33137  xrge0tsmsd  33166  gsumwun  33169  tocyc01  33211  cycpmco2lem4  33222  cycpmco2lem7  33225  cycpmco2  33226  cyc3co2  33233  cycpmrn  33236  archirngz  33282  archiabllem2a  33287  elrgspnlem2  33336  ssdifidllem  33548  ssmxidllem  33565  rprmirred  33623  rprmdvdspow  33625  1arithufdlem3  33638  dfufd2lem  33641  ply1dg3rt0irred  33676  esplyfval1  33749  lindsun  33802  lbsdiflsp0  33803  fldextrspunlsplem  33850  constrmon  33921  constrconj  33922  constrfin  33923  constrelextdg2  33924  constrextdg2lem  33925  zconstr  33941  submateq  33986  lmat22lem  33994  locfinref  34018  xrge0mulc1cn  34118  zrhcntr  34156  qqhval2lem  34158  esumpcvgval  34255  esumcvg  34263  sigaclcu3  34299  measiuns  34394  voliune  34406  volfiniune  34407  volmeas  34408  gsumnunsn  34718  signsply0  34728  signswch  34738  signslema  34739  signstfvneq0  34749  chtvalz  34806  bnj517  35060  bnj1408  35211  bnj1423  35226  bnj1452  35227  weiunse  36681  dnibndlem13  36709  dnibnd  36710  irrdifflemf  37577  poimirlem2  37870  fdc  37993  orel  38350  lsatcvat  39423  lkrpssN  39536  2at0mat0  39898  atmod1i1m  40231  lhp2at0nle  40408  trlcone  41101  tendoex  41348  dihlspsnssN  41705  dochkrsm  41831  lcfl8  41875  lclkrlem2b  41881  lclkrlem2s  41898  lcfrlem21  41936  mapdval2N  42003  mapdspex  42041  aks4d1p5  42447  hashnexinjle  42496  sticksstones12a  42524  sticksstones13  42526  sn-msqgt0d  42853  fimgmcyclem  42900  fsuppind  42945  flt4lem7  43014  nna4b4nsq  43015  pell1qrgaplem  43227  monotoddzzfi  43296  oddcomabszz  43298  zindbi  43300  rmxnn  43305  jm2.24  43317  acongeq  43337  jm2.23  43350  jm2.26lem3  43355  wepwsolem  43396  oe0rif  43639  onmcl  43685  omabs2  43686  omcl2  43687  onsucunipr  43726  oaun3lem1  43728  fzuntgd  43811  frege102d  44107  fnchoice  45386  refsum2cnlem1  45394  wallispilem3  46422  chnsubseqwl  47234  squeezedltsq  47243  wtgoldbnnsum4prm  48159  bgoldbnnsum3prm  48161  nn0sumshdiglem1  48978  mofeu  49204  toslat  49338  2arwcatlem2  49952  2arwcatlem3  49953  2arwcatlem4  49954  2arwcatlem5  49955  2arwcat  49956