Theorem mpjaodan 961

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30473. (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  6430  weniso  7309  isf32lem2  10276  isf32lem4  10278  fpwwe2lem10  10563  fpwwe2lem11  10564  lecasei  11252  ltlecasei  11254  xaddass  13201  xlesubadd  13215  xmulge0  13236  xadddi2  13249  xrsupss  13261  xrinfmss  13262  fzm1  13561  seqf1olem2  14004  expaddzlem  14067  discr  14202  fzomaxdif  15306  iseralt  15647  sumrb  15675  telfsumo  15765  fsumparts  15769  ntrivcvgtail  15865  prodrb  15897  bitsf1  16415  smupvallem  16452  eucalgf  16552  eucalginv  16553  vdwmc2  16950  fvprif  17525  mreexmrid  17609  mreexexlem3d  17612  chnub  18588  chnccats1  18591  chnccat  18592  mulgfval  19045  ressmulgnn0  19053  mulgnn0p1  19061  mulgnn0subcl  19063  mulgsubcl  19064  mulgneg  19068  mulgz  19078  mulgnn0dir  19080  mulgdirlem  19081  mulgdir  19082  submmulg  19094  ghmmulg  19203  odid  19513  oddvds  19522  dfod2  19539  gexid  19556  gexdvds  19559  mulgnn0di  19800  mulgdi  19801  gsumzsplit  19902  2nsgsimpgd  20079  prmgrpsimpgd  20091  lringuplu  20521  lsppratlem5  21149  prmirred  21454  mhpmulcl  22115  1stckgenlem  23518  qtoprest  23682  tgpmulg  24058  tsmssplit  24117  xblss2ps  24366  xblss2  24367  metustfbas  24522  nmoix  24694  nmoleub  24696  idnghm  24708  blcvx  24763  icccmp  24791  xrge0tsms  24800  metdstri  24817  nmoleub2lem  25081  rrxcph  25359  rrxdstprj1  25376  ivthle  25423  ivthle2  25424  dyadmbl  25567  volivth  25574  itg2const2  25708  itg2mulc  25714  dvlip2  25962  dvfsumlem1  25993  mdegmullem  26043  coemulhi  26219  dgrcolem2  26239  coseq00topi  26466  abssinper  26485  cxplea  26660  cxple2  26661  cxple2a  26663  cxpcn3  26712  cxpaddlelem  26715  cxpaddle  26716  ang180lem3  26775  dcubic2  26808  birthdaylem2  26916  jensen  26952  ppiltx  27140  chtub  27175  bcmono  27240  bcmax  27241  bpos  27256  lgseisenlem1  27338  2sqlem4  27384  2sqmod  27399  pntrlog2bndlem5  27544  pntpbnd1  27549  noinfbnd2lem1  27694  noetasuplem4  27700  noetainflem4  27704  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  lemulsd  28130  mulsge0d  28138  mulscan2d  28171  lemuls1ad  28174  absmuls  28236  absnegs  28239  leabss  28240  tgldimor  28570  tgifscgr  28576  tgcgrxfr  28586  tgbtwnconn1  28643  tgbtwnconn2  28644  tgbtwnconn3  28645  tgbtwnconnln3  28646  tgbtwnconn22  28647  tgbtwnconnln1  28648  tgbtwnconnln2  28649  legtrid  28659  legbtwn  28662  tgcgrsub2  28663  legov3  28666  hlln  28675  hltr  28678  btwnhl  28682  ncolncol  28714  mirconn  28746  krippen  28759  midexlem  28760  midex  28805  opphllem2  28816  opphllem5  28819  opphllem6  28820  outpasch  28823  hlpasch  28824  trgcopyeulem  28873  cgrahl  28895  cgracol  28896  ex-natded5.7  30481  ex-natded5.13  30485  ex-natded9.20  30487  ex-natded9.20-2  30488  fconst7v  32693  suppovss  32754  nn0mnfxrd  32824  xrge0infss  32833  xnn0gt0  32842  nn0xmulclb  32844  difioo  32855  iundisjcnt  32871  f1ocnt  32873  fzo0opth  32876  hashxpe  32880  sgncl  32904  sgnmul  32908  nexple  32917  2exple2exp  32918  ccatws1f1o  33011  xrsmulgzz  33069  xrge0addgt0  33077  xrge0adddir  33078  ressmulgnn0d  33105  xrge0tsmsd  33134  gsumwun  33137  tocyc01  33179  cycpmco2lem4  33190  cycpmco2lem7  33193  cycpmco2  33194  cyc3co2  33201  cycpmrn  33204  archirngz  33250  archiabllem2a  33255  elrgspnlem2  33304  ssdifidllem  33516  ssmxidllem  33533  rprmirred  33591  rprmdvdspow  33593  1arithufdlem3  33606  dfufd2lem  33609  ply1dg3rt0irred  33644  esplyfval1  33717  lindsun  33769  lbsdiflsp0  33770  fldextrspunlsplem  33817  constrmon  33888  constrconj  33889  constrfin  33890  constrelextdg2  33891  constrextdg2lem  33892  zconstr  33908  submateq  33953  lmat22lem  33961  locfinref  33985  xrge0mulc1cn  34085  zrhcntr  34123  qqhval2lem  34125  esumpcvgval  34222  esumcvg  34230  sigaclcu3  34266  measiuns  34361  voliune  34373  volfiniune  34374  volmeas  34375  gsumnunsn  34685  signsply0  34695  signswch  34705  signslema  34706  signstfvneq0  34716  chtvalz  34773  bnj517  35027  bnj1408  35178  bnj1423  35193  bnj1452  35194  weiunse  36650  dnibndlem13  36750  dnibnd  36751  irrdifflemf  37639  poimirlem2  37943  fdc  38066  orel  38423  lsatcvat  39496  lkrpssN  39609  2at0mat0  39971  atmod1i1m  40304  lhp2at0nle  40481  trlcone  41174  tendoex  41421  dihlspsnssN  41778  dochkrsm  41904  lcfl8  41948  lclkrlem2b  41954  lclkrlem2s  41971  lcfrlem21  42009  mapdval2N  42076  mapdspex  42114  aks4d1p5  42519  hashnexinjle  42568  sticksstones12a  42596  sticksstones13  42598  sn-msqgt0d  42931  fimgmcyclem  42978  fsuppind  43023  flt4lem7  43092  nna4b4nsq  43093  pell1qrgaplem  43301  monotoddzzfi  43370  oddcomabszz  43372  zindbi  43374  rmxnn  43379  jm2.24  43391  acongeq  43411  jm2.23  43424  jm2.26lem3  43429  wepwsolem  43470  oe0rif  43713  onmcl  43759  omabs2  43760  omcl2  43761  onsucunipr  43800  oaun3lem1  43802  fzuntgd  43885  frege102d  44181  fnchoice  45460  refsum2cnlem1  45468  wallispilem3  46495  chnsubseqwl  47309  squeezedltsq  47318  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  nn0sumshdiglem1  49097  mofeu  49323  toslat  49457  2arwcatlem2  50071  2arwcatlem3  50072  2arwcatlem4  50073  2arwcatlem5  50074  2arwcat  50075