Theorem mpjaodan 960

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30365. (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  6418  weniso  7295  isf32lem2  10267  isf32lem4  10269  fpwwe2lem10  10553  fpwwe2lem11  10554  lecasei  11240  ltlecasei  11242  xaddass  13169  xlesubadd  13183  xmulge0  13204  xadddi2  13217  xrsupss  13229  xrinfmss  13230  fzm1  13528  seqf1olem2  13967  expaddzlem  14030  discr  14165  fzomaxdif  15269  iseralt  15610  sumrb  15638  telfsumo  15727  fsumparts  15731  ntrivcvgtail  15825  prodrb  15857  bitsf1  16375  smupvallem  16412  eucalgf  16512  eucalginv  16513  vdwmc2  16909  fvprif  17483  mreexmrid  17567  mreexexlem3d  17570  mulgfval  18966  ressmulgnn0  18974  mulgnn0p1  18982  mulgnn0subcl  18984  mulgsubcl  18985  mulgneg  18989  mulgz  18999  mulgnn0dir  19001  mulgdirlem  19002  mulgdir  19003  submmulg  19015  ghmmulg  19125  odid  19435  oddvds  19444  dfod2  19461  gexid  19478  gexdvds  19481  mulgnn0di  19722  mulgdi  19723  gsumzsplit  19824  2nsgsimpgd  20001  prmgrpsimpgd  20013  lringuplu  20447  lsppratlem5  21076  prmirred  21399  mhpmulcl  22052  1stckgenlem  23456  qtoprest  23620  tgpmulg  23996  tsmssplit  24055  xblss2ps  24305  xblss2  24306  metustfbas  24461  nmoix  24633  nmoleub  24635  idnghm  24647  blcvx  24702  icccmp  24730  xrge0tsms  24739  metdstri  24756  nmoleub2lem  25030  rrxcph  25308  rrxdstprj1  25325  ivthle  25373  ivthle2  25374  dyadmbl  25517  volivth  25524  itg2const2  25658  itg2mulc  25664  dvlip2  25916  dvfsumlem1  25948  mdegmullem  25999  coemulhi  26175  dgrcolem2  26196  coseq00topi  26427  abssinper  26446  cxplea  26621  cxple2  26622  cxple2a  26624  cxpcn3  26674  cxpaddlelem  26677  cxpaddle  26678  ang180lem3  26737  dcubic2  26770  birthdaylem2  26878  jensen  26915  ppiltx  27103  chtub  27139  bcmono  27204  bcmax  27205  bpos  27220  lgseisenlem1  27302  2sqlem4  27348  2sqmod  27363  pntrlog2bndlem5  27508  pntpbnd1  27513  noinfbnd2lem1  27658  noetasuplem4  27664  noetainflem4  27668  mulsproplem12  28053  mulsproplem13  28054  mulsproplem14  28055  slemuld  28064  mulsge0d  28072  mulscan2d  28105  slemul1ad  28108  absmuls  28169  abssneg  28172  sleabs  28173  tgldimor  28465  tgifscgr  28471  tgcgrxfr  28481  tgbtwnconn1  28538  tgbtwnconn2  28539  tgbtwnconn3  28540  tgbtwnconnln3  28541  tgbtwnconn22  28542  tgbtwnconnln1  28543  tgbtwnconnln2  28544  legtrid  28554  legbtwn  28557  tgcgrsub2  28558  legov3  28561  hlln  28570  hltr  28573  btwnhl  28577  ncolncol  28609  mirconn  28641  krippen  28654  midexlem  28655  midex  28700  opphllem2  28711  opphllem5  28714  opphllem6  28715  outpasch  28718  hlpasch  28719  trgcopyeulem  28768  cgrahl  28790  cgracol  28791  ex-natded5.7  30373  ex-natded5.13  30377  ex-natded9.20  30379  ex-natded9.20-2  30380  suppovss  32637  xrge0infss  32716  xnn0gt0  32725  nn0xmulclb  32727  difioo  32738  iundisjcnt  32754  f1ocnt  32758  fzo0opth  32761  hashxpe  32765  sgncl  32789  sgnmul  32793  nexple  32802  2exple2exp  32803  ccatws1f1o  32906  chnub  32967  chnccats1  32970  xrsmulgzz  32976  xrge0addgt0  32984  xrge0adddir  32985  ressmulgnn0d  33011  xrge0tsmsd  33028  gsumwun  33031  tocyc01  33073  cycpmco2lem4  33084  cycpmco2lem7  33087  cycpmco2  33088  cyc3co2  33095  cycpmrn  33098  archirngz  33144  archiabllem2a  33149  elrgspnlem2  33196  ssdifidllem  33406  ssmxidllem  33423  rprmirred  33481  rprmdvdspow  33483  1arithufdlem3  33496  dfufd2lem  33499  ply1dg3rt0irred  33530  lindsun  33600  lbsdiflsp0  33601  fldextrspunlsplem  33647  constrmon  33713  constrconj  33714  constrfin  33715  constrelextdg2  33716  constrextdg2lem  33717  zconstr  33733  submateq  33778  lmat22lem  33786  locfinref  33810  xrge0mulc1cn  33910  zrhcntr  33948  qqhval2lem  33950  esumpcvgval  34047  esumcvg  34055  sigaclcu3  34091  measiuns  34186  voliune  34198  volfiniune  34199  volmeas  34200  gsumnunsn  34511  signsply0  34521  signswch  34531  signslema  34532  signstfvneq0  34542  chtvalz  34599  bnj517  34854  bnj1408  35005  bnj1423  35020  bnj1452  35021  weiunse  36444  dnibndlem13  36466  dnibnd  36467  irrdifflemf  37301  poimirlem2  37604  fdc  37727  orel  38084  lsatcvat  39031  lkrpssN  39144  2at0mat0  39507  atmod1i1m  39840  lhp2at0nle  40017  trlcone  40710  tendoex  40957  dihlspsnssN  41314  dochkrsm  41440  lcfl8  41484  lclkrlem2b  41490  lclkrlem2s  41507  lcfrlem21  41545  mapdval2N  41612  mapdspex  41650  aks4d1p5  42056  hashnexinjle  42105  sticksstones12a  42133  sticksstones13  42135  sn-msqgt0d  42462  fimgmcyclem  42509  fsuppind  42566  flt4lem7  42635  nna4b4nsq  42636  pell1qrgaplem  42849  monotoddzzfi  42918  oddcomabszz  42920  zindbi  42922  rmxnn  42927  jm2.24  42939  acongeq  42959  jm2.23  42972  jm2.26lem3  42977  wepwsolem  43018  oe0rif  43261  onmcl  43307  omabs2  43308  omcl2  43309  onsucunipr  43348  oaun3lem1  43350  fzuntgd  43434  frege102d  43730  fnchoice  45010  refsum2cnlem1  45018  wallispilem3  46052  squeezedltsq  46874  wtgoldbnnsum4prm  47790  bgoldbnnsum3prm  47792  nn0sumshdiglem1  48610  mofeu  48836  toslat  48970  2arwcatlem2  49585  2arwcatlem3  49586  2arwcatlem4  49587  2arwcatlem5  49588  2arwcat  49589