Theorem mpjaodan 960

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ 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 207  df-an 396  df-or 848

This theorem is referenced by:  onunel  6420  weniso  7296  isf32lem2  10254  isf32lem4  10256  fpwwe2lem10  10540  fpwwe2lem11  10541  lecasei  11228  ltlecasei  11230  xaddass  13152  xlesubadd  13166  xmulge0  13187  xadddi2  13200  xrsupss  13212  xrinfmss  13213  fzm1  13511  seqf1olem2  13953  expaddzlem  14016  discr  14151  fzomaxdif  15255  iseralt  15596  sumrb  15624  telfsumo  15713  fsumparts  15717  ntrivcvgtail  15811  prodrb  15843  bitsf1  16361  smupvallem  16398  eucalgf  16498  eucalginv  16499  vdwmc2  16895  fvprif  17469  mreexmrid  17553  mreexexlem3d  17556  chnub  18532  chnccats1  18535  chnccat  18536  mulgfval  18986  ressmulgnn0  18994  mulgnn0p1  19002  mulgnn0subcl  19004  mulgsubcl  19005  mulgneg  19009  mulgz  19019  mulgnn0dir  19021  mulgdirlem  19022  mulgdir  19023  submmulg  19035  ghmmulg  19144  odid  19454  oddvds  19463  dfod2  19480  gexid  19497  gexdvds  19500  mulgnn0di  19741  mulgdi  19742  gsumzsplit  19843  2nsgsimpgd  20020  prmgrpsimpgd  20032  lringuplu  20463  lsppratlem5  21092  prmirred  21415  mhpmulcl  22067  1stckgenlem  23471  qtoprest  23635  tgpmulg  24011  tsmssplit  24070  xblss2ps  24319  xblss2  24320  metustfbas  24475  nmoix  24647  nmoleub  24649  idnghm  24661  blcvx  24716  icccmp  24744  xrge0tsms  24753  metdstri  24770  nmoleub2lem  25044  rrxcph  25322  rrxdstprj1  25339  ivthle  25387  ivthle2  25388  dyadmbl  25531  volivth  25538  itg2const2  25672  itg2mulc  25678  dvlip2  25930  dvfsumlem1  25962  mdegmullem  26013  coemulhi  26189  dgrcolem2  26210  coseq00topi  26441  abssinper  26460  cxplea  26635  cxple2  26636  cxple2a  26638  cxpcn3  26688  cxpaddlelem  26691  cxpaddle  26692  ang180lem3  26751  dcubic2  26784  birthdaylem2  26892  jensen  26929  ppiltx  27117  chtub  27153  bcmono  27218  bcmax  27219  bpos  27234  lgseisenlem1  27316  2sqlem4  27362  2sqmod  27377  pntrlog2bndlem5  27522  pntpbnd1  27527  noinfbnd2lem1  27672  noetasuplem4  27678  noetainflem4  27682  mulsproplem12  28069  mulsproplem13  28070  mulsproplem14  28071  slemuld  28080  mulsge0d  28088  mulscan2d  28121  slemul1ad  28124  absmuls  28185  abssneg  28188  sleabs  28189  tgldimor  28483  tgifscgr  28489  tgcgrxfr  28499  tgbtwnconn1  28556  tgbtwnconn2  28557  tgbtwnconn3  28558  tgbtwnconnln3  28559  tgbtwnconn22  28560  tgbtwnconnln1  28561  tgbtwnconnln2  28562  legtrid  28572  legbtwn  28575  tgcgrsub2  28576  legov3  28579  hlln  28588  hltr  28591  btwnhl  28595  ncolncol  28627  mirconn  28659  krippen  28672  midexlem  28673  midex  28718  opphllem2  28729  opphllem5  28732  opphllem6  28733  outpasch  28736  hlpasch  28737  trgcopyeulem  28786  cgrahl  28808  cgracol  28809  ex-natded5.7  30395  ex-natded5.13  30399  ex-natded9.20  30401  ex-natded9.20-2  30402  fconst7v  32607  suppovss  32668  xrge0infss  32749  xnn0gt0  32758  nn0xmulclb  32760  difioo  32771  iundisjcnt  32787  f1ocnt  32789  fzo0opth  32792  hashxpe  32796  sgncl  32821  sgnmul  32825  nexple  32834  2exple2exp  32835  ccatws1f1o  32941  xrsmulgzz  32999  xrge0addgt0  33007  xrge0adddir  33008  ressmulgnn0d  33034  xrge0tsmsd  33051  gsumwun  33054  tocyc01  33096  cycpmco2lem4  33107  cycpmco2lem7  33110  cycpmco2  33111  cyc3co2  33118  cycpmrn  33121  archirngz  33167  archiabllem2a  33172  elrgspnlem2  33219  ssdifidllem  33430  ssmxidllem  33447  rprmirred  33505  rprmdvdspow  33507  1arithufdlem3  33520  dfufd2lem  33523  ply1dg3rt0irred  33555  lindsun  33661  lbsdiflsp0  33662  fldextrspunlsplem  33709  constrmon  33780  constrconj  33781  constrfin  33782  constrelextdg2  33783  constrextdg2lem  33784  zconstr  33800  submateq  33845  lmat22lem  33853  locfinref  33877  xrge0mulc1cn  33977  zrhcntr  34015  qqhval2lem  34017  esumpcvgval  34114  esumcvg  34122  sigaclcu3  34158  measiuns  34253  voliune  34265  volfiniune  34266  volmeas  34267  gsumnunsn  34577  signsply0  34587  signswch  34597  signslema  34598  signstfvneq0  34608  chtvalz  34665  bnj517  34920  bnj1408  35071  bnj1423  35086  bnj1452  35087  weiunse  36535  dnibndlem13  36557  dnibnd  36558  irrdifflemf  37392  poimirlem2  37685  fdc  37808  orel  38165  lsatcvat  39172  lkrpssN  39285  2at0mat0  39647  atmod1i1m  39980  lhp2at0nle  40157  trlcone  40850  tendoex  41097  dihlspsnssN  41454  dochkrsm  41580  lcfl8  41624  lclkrlem2b  41630  lclkrlem2s  41647  lcfrlem21  41685  mapdval2N  41752  mapdspex  41790  aks4d1p5  42196  hashnexinjle  42245  sticksstones12a  42273  sticksstones13  42275  sn-msqgt0d  42607  fimgmcyclem  42654  fsuppind  42711  flt4lem7  42780  nna4b4nsq  42781  pell1qrgaplem  42993  monotoddzzfi  43062  oddcomabszz  43064  zindbi  43066  rmxnn  43071  jm2.24  43083  acongeq  43103  jm2.23  43116  jm2.26lem3  43121  wepwsolem  43162  oe0rif  43405  onmcl  43451  omabs2  43452  omcl2  43453  onsucunipr  43492  oaun3lem1  43494  fzuntgd  43578  frege102d  43874  fnchoice  45153  refsum2cnlem1  45161  wallispilem3  46192  chnsubseqwl  47004  squeezedltsq  47013  wtgoldbnnsum4prm  47929  bgoldbnnsum3prm  47931  nn0sumshdiglem1  48749  mofeu  48975  toslat  49109  2arwcatlem2  49724  2arwcatlem3  49725  2arwcatlem4  49726  2arwcatlem5  49727  2arwcat  49728