Theorem mpjaodan 960

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30390. (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  6419  weniso  7294  isf32lem2  10251  isf32lem4  10253  fpwwe2lem10  10537  fpwwe2lem11  10538  lecasei  11225  ltlecasei  11227  xaddass  13154  xlesubadd  13168  xmulge0  13189  xadddi2  13202  xrsupss  13214  xrinfmss  13215  fzm1  13513  seqf1olem2  13955  expaddzlem  14018  discr  14153  fzomaxdif  15257  iseralt  15598  sumrb  15626  telfsumo  15715  fsumparts  15719  ntrivcvgtail  15813  prodrb  15845  bitsf1  16363  smupvallem  16400  eucalgf  16500  eucalginv  16501  vdwmc2  16897  fvprif  17471  mreexmrid  17555  mreexexlem3d  17558  chnub  18534  chnccats1  18537  chnccat  18538  mulgfval  18988  ressmulgnn0  18996  mulgnn0p1  19004  mulgnn0subcl  19006  mulgsubcl  19007  mulgneg  19011  mulgz  19021  mulgnn0dir  19023  mulgdirlem  19024  mulgdir  19025  submmulg  19037  ghmmulg  19146  odid  19456  oddvds  19465  dfod2  19482  gexid  19499  gexdvds  19502  mulgnn0di  19743  mulgdi  19744  gsumzsplit  19845  2nsgsimpgd  20022  prmgrpsimpgd  20034  lringuplu  20465  lsppratlem5  21094  prmirred  21417  mhpmulcl  22070  1stckgenlem  23474  qtoprest  23638  tgpmulg  24014  tsmssplit  24073  xblss2ps  24322  xblss2  24323  metustfbas  24478  nmoix  24650  nmoleub  24652  idnghm  24664  blcvx  24719  icccmp  24747  xrge0tsms  24756  metdstri  24773  nmoleub2lem  25047  rrxcph  25325  rrxdstprj1  25342  ivthle  25390  ivthle2  25391  dyadmbl  25534  volivth  25541  itg2const2  25675  itg2mulc  25681  dvlip2  25933  dvfsumlem1  25965  mdegmullem  26016  coemulhi  26192  dgrcolem2  26213  coseq00topi  26444  abssinper  26463  cxplea  26638  cxple2  26639  cxple2a  26641  cxpcn3  26691  cxpaddlelem  26694  cxpaddle  26695  ang180lem3  26754  dcubic2  26787  birthdaylem2  26895  jensen  26932  ppiltx  27120  chtub  27156  bcmono  27221  bcmax  27222  bpos  27237  lgseisenlem1  27319  2sqlem4  27365  2sqmod  27380  pntrlog2bndlem5  27525  pntpbnd1  27530  noinfbnd2lem1  27675  noetasuplem4  27681  noetainflem4  27685  mulsproplem12  28072  mulsproplem13  28073  mulsproplem14  28074  slemuld  28083  mulsge0d  28091  mulscan2d  28124  slemul1ad  28127  absmuls  28188  abssneg  28191  sleabs  28192  tgldimor  28486  tgifscgr  28492  tgcgrxfr  28502  tgbtwnconn1  28559  tgbtwnconn2  28560  tgbtwnconn3  28561  tgbtwnconnln3  28562  tgbtwnconn22  28563  tgbtwnconnln1  28564  tgbtwnconnln2  28565  legtrid  28575  legbtwn  28578  tgcgrsub2  28579  legov3  28582  hlln  28591  hltr  28594  btwnhl  28598  ncolncol  28630  mirconn  28662  krippen  28675  midexlem  28676  midex  28721  opphllem2  28732  opphllem5  28735  opphllem6  28736  outpasch  28739  hlpasch  28740  trgcopyeulem  28789  cgrahl  28811  cgracol  28812  ex-natded5.7  30398  ex-natded5.13  30402  ex-natded9.20  30404  ex-natded9.20-2  30405  fconst7v  32610  suppovss  32669  xrge0infss  32750  xnn0gt0  32759  nn0xmulclb  32761  difioo  32772  iundisjcnt  32787  f1ocnt  32789  fzo0opth  32792  hashxpe  32796  sgncl  32821  sgnmul  32825  nexple  32834  2exple2exp  32835  ccatws1f1o  32939  xrsmulgzz  32997  xrge0addgt0  33005  xrge0adddir  33006  ressmulgnn0d  33032  xrge0tsmsd  33049  gsumwun  33052  tocyc01  33094  cycpmco2lem4  33105  cycpmco2lem7  33108  cycpmco2  33109  cyc3co2  33116  cycpmrn  33119  archirngz  33165  archiabllem2a  33170  elrgspnlem2  33217  ssdifidllem  33428  ssmxidllem  33445  rprmirred  33503  rprmdvdspow  33505  1arithufdlem3  33518  dfufd2lem  33521  ply1dg3rt0irred  33553  lindsun  33645  lbsdiflsp0  33646  fldextrspunlsplem  33693  constrmon  33764  constrconj  33765  constrfin  33766  constrelextdg2  33767  constrextdg2lem  33768  zconstr  33784  submateq  33829  lmat22lem  33837  locfinref  33861  xrge0mulc1cn  33961  zrhcntr  33999  qqhval2lem  34001  esumpcvgval  34098  esumcvg  34106  sigaclcu3  34142  measiuns  34237  voliune  34249  volfiniune  34250  volmeas  34251  gsumnunsn  34561  signsply0  34571  signswch  34581  signslema  34582  signstfvneq0  34592  chtvalz  34649  bnj517  34904  bnj1408  35055  bnj1423  35070  bnj1452  35071  weiunse  36519  dnibndlem13  36541  dnibnd  36542  irrdifflemf  37376  poimirlem2  37668  fdc  37791  orel  38148  lsatcvat  39155  lkrpssN  39268  2at0mat0  39630  atmod1i1m  39963  lhp2at0nle  40140  trlcone  40833  tendoex  41080  dihlspsnssN  41437  dochkrsm  41563  lcfl8  41607  lclkrlem2b  41613  lclkrlem2s  41630  lcfrlem21  41668  mapdval2N  41735  mapdspex  41773  aks4d1p5  42179  hashnexinjle  42228  sticksstones12a  42256  sticksstones13  42258  sn-msqgt0d  42585  fimgmcyclem  42632  fsuppind  42689  flt4lem7  42758  nna4b4nsq  42759  pell1qrgaplem  42971  monotoddzzfi  43040  oddcomabszz  43042  zindbi  43044  rmxnn  43049  jm2.24  43061  acongeq  43081  jm2.23  43094  jm2.26lem3  43099  wepwsolem  43140  oe0rif  43383  onmcl  43429  omabs2  43430  omcl2  43431  onsucunipr  43470  oaun3lem1  43472  fzuntgd  43556  frege102d  43852  fnchoice  45131  refsum2cnlem1  45139  wallispilem3  46170  chnsubseqwl  46982  squeezedltsq  46991  wtgoldbnnsum4prm  47907  bgoldbnnsum3prm  47909  nn0sumshdiglem1  48727  mofeu  48953  toslat  49087  2arwcatlem2  49702  2arwcatlem3  49703  2arwcatlem4  49704  2arwcatlem5  49705  2arwcat  49706