Theorem mpjaodan 973

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

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  onunel  6470  weniso  7354  isf32lem2  10339  isf32lem4  10341  fpwwe2lem10  10626  fpwwe2lem11  10627  lecasei  11317  ltlecasei  11319  xaddass  13276  xlesubadd  13290  xmulge0  13311  xadddi2  13324  xrsupss  13336  xrinfmss  13337  fzm1  13637  seqf1olem2  14080  expaddzlem  14143  discr  14278  sgncl  15136  sgnmul  15146  fzomaxdif  15397  iseralt  15738  sumrb  15766  telfsumo  15856  fsumparts  15860  ntrivcvgtail  15956  prodrb  15988  bitsf1  16505  smupvallem  16542  eucalgf  16642  eucalginv  16643  vdwmc2  17040  fvprif  17616  mreexmrid  17700  mreexexlem3d  17703  chnub  18679  chnccats1  18682  chnccat  18683  mulgfval  19136  ressmulgnn0  19144  mulgnn0p1  19152  mulgnn0subcl  19154  mulgsubcl  19155  mulgneg  19159  mulgz  19169  mulgnn0dir  19171  mulgdirlem  19172  mulgdir  19173  submmulg  19185  ghmmulg  19299  odid  19609  oddvds  19618  dfod2  19635  gexid  19652  gexdvds  19655  mulgnn0di  19896  mulgdi  19897  gsumzsplit  19998  2nsgsimpgd  20175  prmgrpsimpgd  20187  lringuplu  20630  lsppratlem5  21256  ssdifidllem  21465  prmirred  21605  mhpmulcl  22293  1stckgenlem  23691  qtoprest  23855  tgpmulg  24231  tsmssplit  24290  xblss2ps  24539  xblss2  24540  metustfbas  24695  nmoix  24867  nmoleub  24869  idnghm  24881  blcvx  24936  icccmp  24964  xrge0tsms  24973  metdstri  24990  nmoleub2lem  25254  rrxcph  25532  rrxdstprj1  25549  ivthle  25596  ivthle2  25597  dyadmbl  25740  volivth  25747  itg2const2  25881  itg2mulc  25887  dvlip2  26135  dvfsumlem1  26166  mdegmullem  26216  coemulhi  26392  dgrcolem2  26412  coseq00topi  26648  abssinper  26667  cxplea  26842  cxple2  26843  cxple2a  26845  cxpcn3  26894  cxpaddlelem  26897  cxpaddle  26898  ang180lem3  26957  dcubic2  26990  birthdaylem2  27098  jensen  27134  ppiltx  27322  chtub  27357  bcmono  27422  bcmax  27423  bpos  27438  lgseisenlem1  27520  2sqlem4  27566  2sqmod  27581  pntrlog2bndlem5  27726  pntpbnd1  27731  noinfbnd2lem1  27875  noetasuplem4  27881  noetainflem4  27885  mulsproplem12  28301  mulsproplem13  28302  mulsproplem14  28303  lemulsd  28312  mulsge0d  28320  mulscan2d  28353  lemuls1ad  28356  absmuls  28418  absnegs  28421  leabss  28422  tgldimor  28752  tgifscgr  28758  tgcgrxfr  28768  tgbtwnconn1  28825  tgbtwnconn2  28826  tgbtwnconn3  28827  tgbtwnconnln3  28828  tgbtwnconn22  28829  tgbtwnconnln1  28830  tgbtwnconnln2  28831  legtrid  28841  legbtwn  28844  tgcgrsub2  28845  legov3  28848  hlln  28860  hltr  28863  btwnhl  28867  ncolncol  28901  mirconn  28936  krippen  28949  midexlem  28950  midex  28999  opphllem2  29010  opphllem5  29013  opphllem6  29014  outpasch  29018  hlpasch  29019  plngcplem  29048  plngrotlem1  29050  plngrotlem2  29051  lnssplng  29055  trgcopyeulem  29097  cgrahl  29119  cgracol  29120  prlngmolem2  29184  ex-natded5.7  30743  ex-natded5.13  30747  ex-natded9.20  30749  ex-natded9.20-2  30750  fconst7v  32946  suppovss  33007  nn0mnfxrd  33077  xrge0infss  33086  xnn0gt0  33095  nn0xmulclb  33097  difioo  33108  iundisjcnt  33124  f1ocnt  33126  fzo0opth  33129  hashxpe  33133  nexple  33158  2exple2exp  33159  ccatws1f1o  33252  xrsmulgzz  33310  xrge0addgt0  33318  xrge0adddir  33319  ressmulgnn0d  33345  xrge0tsmsd  33374  gsumwun  33377  tocyc01  33419  cycpmco2lem4  33430  cycpmco2lem7  33433  cycpmco2  33434  cyc3co2  33441  cycpmrn  33444  archirngz  33490  archiabllem2a  33495  elrgspnlem2  33544  ssmxidllem  33737  rprmirred  33802  rprmdvdspow  33804  1arithufdlem3  33817  dfufd2lem  33820  ply1dg3rt0irred  33855  esplyfval1  33944  lindsun  33996  lbsdiflsp0  33997  fldextrspunlsplem  34044  constrmon  34115  constrconj  34116  constrfin  34117  constrelextdg2  34118  constrextdg2lem  34119  zconstr  34135  submateq  34180  lmat22lem  34188  locfinref  34212  xrge0mulc1cn  34312  zrhcntr  34350  qqhval2lem  34352  esumpcvgval  34449  esumcvg  34457  sigaclcu3  34493  measiuns  34588  voliune  34600  volfiniune  34601  volmeas  34602  gsumnunsn  34912  signsply0  34919  signswch  34929  signslema  34930  signstfvneq0  34940  chtvalz  34997  btwnlng13  35038  bnj517  35254  bnj1408  35405  bnj1423  35420  bnj1452  35421  weiunse  36960  dnibndlem13  37060  dnibnd  37061  irrdifflemf  37950  poimirlem2  38254  fdc  38377  orel  38732  lsatcvat  39805  lkrpssN  39918  2at0mat0  40280  atmod1i1m  40613  lhp2at0nle  40790  trlcone  41483  tendoex  41730  dihlspsnssN  42087  dochkrsm  42213  lcfl8  42257  lclkrlem2b  42263  lclkrlem2s  42280  lcfrlem21  42318  mapdval2N  42385  mapdspex  42423  aks4d1p5  42828  hashnexinjle  42877  sticksstones12a  42905  sticksstones13  42907  sn-msqgt0d  43241  fimgmcyclem  43284  fsuppind  43305  flt4lem7  43374  nna4b4nsq  43375  pell1qrgaplem  43583  monotoddzzfi  43652  oddcomabszz  43654  zindbi  43656  rmxnn  43661  jm2.24  43673  acongeq  43693  jm2.23  43706  jm2.26lem3  43711  wepwsolem  43752  oe0rif  43995  onmcl  44041  omabs2  44042  omcl2  44043  onsucunipr  44082  oaun3lem1  44084  fzuntgd  44167  frege102d  44463  fnchoice  45732  refsum2cnlem1  45740  wallispilem3  46764  chnsubseqwl  47578  squeezedltsq  47586  wtgoldbnnsum4prm  48550  bgoldbnnsum3prm  48552  nn0sumshdiglem1  49384  mofeu  49609  toslat  49743  2arwcatlem2  50357  2arwcatlem3  50358  2arwcatlem4  50359  2arwcatlem5  50360  2arwcat  50361