Theorem mpjaodan 961

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30488. (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  6424  weniso  7302  isf32lem2  10267  isf32lem4  10269  fpwwe2lem10  10554  fpwwe2lem11  10555  lecasei  11243  ltlecasei  11245  xaddass  13192  xlesubadd  13206  xmulge0  13227  xadddi2  13240  xrsupss  13252  xrinfmss  13253  fzm1  13552  seqf1olem2  13995  expaddzlem  14058  discr  14193  fzomaxdif  15297  iseralt  15638  sumrb  15666  telfsumo  15756  fsumparts  15760  ntrivcvgtail  15856  prodrb  15888  bitsf1  16406  smupvallem  16443  eucalgf  16543  eucalginv  16544  vdwmc2  16941  fvprif  17516  mreexmrid  17600  mreexexlem3d  17603  chnub  18579  chnccats1  18582  chnccat  18583  mulgfval  19036  ressmulgnn0  19044  mulgnn0p1  19052  mulgnn0subcl  19054  mulgsubcl  19055  mulgneg  19059  mulgz  19069  mulgnn0dir  19071  mulgdirlem  19072  mulgdir  19073  submmulg  19085  ghmmulg  19194  odid  19504  oddvds  19513  dfod2  19530  gexid  19547  gexdvds  19550  mulgnn0di  19791  mulgdi  19792  gsumzsplit  19893  2nsgsimpgd  20070  prmgrpsimpgd  20082  lringuplu  20512  lsppratlem5  21141  prmirred  21464  mhpmulcl  22125  1stckgenlem  23528  qtoprest  23692  tgpmulg  24068  tsmssplit  24127  xblss2ps  24376  xblss2  24377  metustfbas  24532  nmoix  24704  nmoleub  24706  idnghm  24718  blcvx  24773  icccmp  24801  xrge0tsms  24810  metdstri  24827  nmoleub2lem  25091  rrxcph  25369  rrxdstprj1  25386  ivthle  25433  ivthle2  25434  dyadmbl  25577  volivth  25584  itg2const2  25718  itg2mulc  25724  dvlip2  25972  dvfsumlem1  26003  mdegmullem  26053  coemulhi  26229  dgrcolem2  26249  coseq00topi  26479  abssinper  26498  cxplea  26673  cxple2  26674  cxple2a  26676  cxpcn3  26725  cxpaddlelem  26728  cxpaddle  26729  ang180lem3  26788  dcubic2  26821  birthdaylem2  26929  jensen  26966  ppiltx  27154  chtub  27189  bcmono  27254  bcmax  27255  bpos  27270  lgseisenlem1  27352  2sqlem4  27398  2sqmod  27413  pntrlog2bndlem5  27558  pntpbnd1  27563  noinfbnd2lem1  27708  noetasuplem4  27714  noetainflem4  27718  mulsproplem12  28133  mulsproplem13  28134  mulsproplem14  28135  lemulsd  28144  mulsge0d  28152  mulscan2d  28185  lemuls1ad  28188  absmuls  28250  absnegs  28253  leabss  28254  tgldimor  28584  tgifscgr  28590  tgcgrxfr  28600  tgbtwnconn1  28657  tgbtwnconn2  28658  tgbtwnconn3  28659  tgbtwnconnln3  28660  tgbtwnconn22  28661  tgbtwnconnln1  28662  tgbtwnconnln2  28663  legtrid  28673  legbtwn  28676  tgcgrsub2  28677  legov3  28680  hlln  28689  hltr  28692  btwnhl  28696  ncolncol  28728  mirconn  28760  krippen  28773  midexlem  28774  midex  28819  opphllem2  28830  opphllem5  28833  opphllem6  28834  outpasch  28837  hlpasch  28838  trgcopyeulem  28887  cgrahl  28909  cgracol  28910  ex-natded5.7  30496  ex-natded5.13  30500  ex-natded9.20  30502  ex-natded9.20-2  30503  fconst7v  32708  suppovss  32769  nn0mnfxrd  32839  xrge0infss  32848  xnn0gt0  32857  nn0xmulclb  32859  difioo  32870  iundisjcnt  32886  f1ocnt  32888  fzo0opth  32891  hashxpe  32895  sgncl  32919  sgnmul  32923  nexple  32932  2exple2exp  32933  ccatws1f1o  33026  xrsmulgzz  33084  xrge0addgt0  33092  xrge0adddir  33093  ressmulgnn0d  33120  xrge0tsmsd  33149  gsumwun  33152  tocyc01  33194  cycpmco2lem4  33205  cycpmco2lem7  33208  cycpmco2  33209  cyc3co2  33216  cycpmrn  33219  archirngz  33265  archiabllem2a  33270  elrgspnlem2  33319  ssdifidllem  33531  ssmxidllem  33548  rprmirred  33606  rprmdvdspow  33608  1arithufdlem3  33621  dfufd2lem  33624  ply1dg3rt0irred  33659  esplyfval1  33732  lindsun  33785  lbsdiflsp0  33786  fldextrspunlsplem  33833  constrmon  33904  constrconj  33905  constrfin  33906  constrelextdg2  33907  constrextdg2lem  33908  zconstr  33924  submateq  33969  lmat22lem  33977  locfinref  34001  xrge0mulc1cn  34101  zrhcntr  34139  qqhval2lem  34141  esumpcvgval  34238  esumcvg  34246  sigaclcu3  34282  measiuns  34377  voliune  34389  volfiniune  34390  volmeas  34391  gsumnunsn  34701  signsply0  34711  signswch  34721  signslema  34722  signstfvneq0  34732  chtvalz  34789  bnj517  35043  bnj1408  35194  bnj1423  35209  bnj1452  35210  weiunse  36666  dnibndlem13  36766  dnibnd  36767  irrdifflemf  37655  poimirlem2  37957  fdc  38080  orel  38437  lsatcvat  39510  lkrpssN  39623  2at0mat0  39985  atmod1i1m  40318  lhp2at0nle  40495  trlcone  41188  tendoex  41435  dihlspsnssN  41792  dochkrsm  41918  lcfl8  41962  lclkrlem2b  41968  lclkrlem2s  41985  lcfrlem21  42023  mapdval2N  42090  mapdspex  42128  aks4d1p5  42533  hashnexinjle  42582  sticksstones12a  42610  sticksstones13  42612  sn-msqgt0d  42945  fimgmcyclem  42992  fsuppind  43037  flt4lem7  43106  nna4b4nsq  43107  pell1qrgaplem  43319  monotoddzzfi  43388  oddcomabszz  43390  zindbi  43392  rmxnn  43397  jm2.24  43409  acongeq  43429  jm2.23  43442  jm2.26lem3  43447  wepwsolem  43488  oe0rif  43731  onmcl  43777  omabs2  43778  omcl2  43779  onsucunipr  43818  oaun3lem1  43820  fzuntgd  43903  frege102d  44199  fnchoice  45478  refsum2cnlem1  45486  wallispilem3  46513  chnsubseqwl  47325  squeezedltsq  47334  wtgoldbnnsum4prm  48290  bgoldbnnsum3prm  48292  nn0sumshdiglem1  49109  mofeu  49335  toslat  49469  2arwcatlem2  50083  2arwcatlem3  50084  2arwcatlem4  50085  2arwcatlem5  50086  2arwcat  50087