Theorem mpjaodan 973

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30663. (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 972	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
5	1, 4	mpdan 699	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860

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-an 401  df-or 861

This theorem is referenced by:  onunel  6457  weniso  7342  isf32lem2  10326  isf32lem4  10328  fpwwe2lem10  10613  fpwwe2lem11  10614  lecasei  11304  ltlecasei  11306  xaddass  13266  xlesubadd  13280  xmulge0  13301  xadddi2  13314  xrsupss  13326  xrinfmss  13327  fzm1  13626  seqf1olem2  14069  expaddzlem  14132  discr  14267  sgncl  15124  sgnmul  15134  fzomaxdif  15385  iseralt  15726  sumrb  15754  telfsumo  15844  fsumparts  15848  ntrivcvgtail  15944  prodrb  15976  bitsf1  16494  smupvallem  16531  eucalgf  16631  eucalginv  16632  vdwmc2  17029  fvprif  17605  mreexmrid  17689  mreexexlem3d  17692  chnub  18668  chnccats1  18671  chnccat  18672  mulgfval  19126  ressmulgnn0  19134  mulgnn0p1  19142  mulgnn0subcl  19144  mulgsubcl  19145  mulgneg  19149  mulgz  19159  mulgnn0dir  19161  mulgdirlem  19162  mulgdir  19163  submmulg  19175  ghmmulg  19289  odid  19599  oddvds  19608  dfod2  19625  gexid  19642  gexdvds  19645  mulgnn0di  19886  mulgdi  19887  gsumzsplit  19988  2nsgsimpgd  20165  prmgrpsimpgd  20177  lringuplu  20620  lsppratlem5  21244  ssdifidllem  21444  prmirred  21584  mhpmulcl  22272  1stckgenlem  23671  qtoprest  23835  tgpmulg  24211  tsmssplit  24270  xblss2ps  24519  xblss2  24520  metustfbas  24675  nmoix  24847  nmoleub  24849  idnghm  24861  blcvx  24916  icccmp  24944  xrge0tsms  24953  metdstri  24970  nmoleub2lem  25234  rrxcph  25512  rrxdstprj1  25529  ivthle  25576  ivthle2  25577  dyadmbl  25720  volivth  25727  itg2const2  25861  itg2mulc  25867  dvlip2  26115  dvfsumlem1  26146  mdegmullem  26196  coemulhi  26372  dgrcolem2  26392  coseq00topi  26625  abssinper  26644  cxplea  26819  cxple2  26820  cxple2a  26822  cxpcn3  26871  cxpaddlelem  26874  cxpaddle  26875  ang180lem3  26934  dcubic2  26967  birthdaylem2  27075  jensen  27111  ppiltx  27299  chtub  27334  bcmono  27399  bcmax  27400  bpos  27415  lgseisenlem1  27497  2sqlem4  27543  2sqmod  27558  pntrlog2bndlem5  27703  pntpbnd1  27708  noinfbnd2lem1  27852  noetasuplem4  27858  noetainflem4  27862  mulsproplem12  28278  mulsproplem13  28279  mulsproplem14  28280  lemulsd  28289  mulsge0d  28297  mulscan2d  28330  lemuls1ad  28333  absmuls  28395  absnegs  28398  leabss  28399  tgldimor  28729  tgifscgr  28735  tgcgrxfr  28745  tgbtwnconn1  28802  tgbtwnconn2  28803  tgbtwnconn3  28804  tgbtwnconnln3  28805  tgbtwnconn22  28806  tgbtwnconnln1  28807  tgbtwnconnln2  28808  legtrid  28818  legbtwn  28821  tgcgrsub2  28822  legov3  28825  hlln  28834  hltr  28837  btwnhl  28841  ncolncol  28874  mirconn  28909  krippen  28922  midexlem  28923  midex  28968  opphllem2  28979  opphllem5  28982  opphllem6  28983  outpasch  28986  hlpasch  28987  plngcplem  29015  plngrotlem1  29017  plngrotlem2  29018  lnssplng  29022  trgcopyeulem  29057  cgrahl  29079  cgracol  29080  ex-natded5.7  30671  ex-natded5.13  30675  ex-natded9.20  30677  ex-natded9.20-2  30678  fconst7v  32877  suppovss  32938  nn0mnfxrd  33008  xrge0infss  33017  xnn0gt0  33026  nn0xmulclb  33028  difioo  33039  iundisjcnt  33055  f1ocnt  33057  fzo0opth  33060  hashxpe  33064  nexple  33090  2exple2exp  33091  ccatws1f1o  33184  xrsmulgzz  33242  xrge0addgt0  33250  xrge0adddir  33251  ressmulgnn0d  33277  xrge0tsmsd  33306  gsumwun  33309  tocyc01  33351  cycpmco2lem4  33362  cycpmco2lem7  33365  cycpmco2  33366  cyc3co2  33373  cycpmrn  33376  archirngz  33422  archiabllem2a  33427  elrgspnlem2  33476  ssmxidllem  33673  rprmirred  33738  rprmdvdspow  33740  1arithufdlem3  33753  dfufd2lem  33756  ply1dg3rt0irred  33791  esplyfval1  33880  lindsun  33932  lbsdiflsp0  33933  fldextrspunlsplem  33980  constrmon  34051  constrconj  34052  constrfin  34053  constrelextdg2  34054  constrextdg2lem  34055  zconstr  34071  submateq  34116  lmat22lem  34124  locfinref  34148  xrge0mulc1cn  34248  zrhcntr  34286  qqhval2lem  34288  esumpcvgval  34385  esumcvg  34393  sigaclcu3  34429  measiuns  34524  voliune  34536  volfiniune  34537  volmeas  34538  gsumnunsn  34848  signsply0  34855  signswch  34865  signslema  34866  signstfvneq0  34876  chtvalz  34933  btwnlng13  34974  bnj517  35190  bnj1408  35341  bnj1423  35356  bnj1452  35357  weiunse  36841  dnibndlem13  36941  dnibnd  36942  irrdifflemf  37829  poimirlem2  38133  fdc  38256  orel  38613  lsatcvat  39686  lkrpssN  39799  2at0mat0  40161  atmod1i1m  40494  lhp2at0nle  40671  trlcone  41364  tendoex  41611  dihlspsnssN  41968  dochkrsm  42094  lcfl8  42138  lclkrlem2b  42144  lclkrlem2s  42161  lcfrlem21  42199  mapdval2N  42266  mapdspex  42304  aks4d1p5  42709  hashnexinjle  42758  sticksstones12a  42786  sticksstones13  42788  sn-msqgt0d  43120  fimgmcyclem  43163  fsuppind  43184  flt4lem7  43253  nna4b4nsq  43254  pell1qrgaplem  43462  monotoddzzfi  43531  oddcomabszz  43533  zindbi  43535  rmxnn  43540  jm2.24  43552  acongeq  43572  jm2.23  43585  jm2.26lem3  43590  wepwsolem  43631  oe0rif  43874  onmcl  43920  omabs2  43921  omcl2  43922  onsucunipr  43961  oaun3lem1  43963  fzuntgd  44046  frege102d  44342  fnchoice  45607  refsum2cnlem1  45615  wallispilem3  46639  chnsubseqwl  47453  squeezedltsq  47462  wtgoldbnnsum4prm  48422  bgoldbnnsum3prm  48424  nn0sumshdiglem1  49252  mofeu  49477  toslat  49611  2arwcatlem2  50225  2arwcatlem3  50226  2arwcatlem4  50227  2arwcatlem5  50228  2arwcat  50229