Theorem mpjaodan 971

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

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 858

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 209  df-an 400  df-or 859

This theorem is referenced by:  onunel  6449  weniso  7334  isf32lem2  10308  isf32lem4  10310  fpwwe2lem10  10595  fpwwe2lem11  10596  lecasei  11286  ltlecasei  11288  xaddass  13249  xlesubadd  13263  xmulge0  13284  xadddi2  13297  xrsupss  13309  xrinfmss  13310  fzm1  13609  seqf1olem2  14052  expaddzlem  14115  discr  14250  fzomaxdif  15354  iseralt  15695  sumrb  15723  telfsumo  15813  fsumparts  15817  ntrivcvgtail  15913  prodrb  15945  bitsf1  16463  smupvallem  16500  eucalgf  16600  eucalginv  16601  vdwmc2  16998  fvprif  17574  mreexmrid  17658  mreexexlem3d  17661  chnub  18637  chnccats1  18640  chnccat  18641  mulgfval  19094  ressmulgnn0  19102  mulgnn0p1  19110  mulgnn0subcl  19112  mulgsubcl  19113  mulgneg  19117  mulgz  19127  mulgnn0dir  19129  mulgdirlem  19130  mulgdir  19131  submmulg  19143  ghmmulg  19251  odid  19561  oddvds  19570  dfod2  19587  gexid  19604  gexdvds  19607  mulgnn0di  19848  mulgdi  19849  gsumzsplit  19950  2nsgsimpgd  20127  prmgrpsimpgd  20139  lringuplu  20573  lsppratlem5  21201  prmirred  21506  mhpmulcl  22194  1stckgenlem  23593  qtoprest  23757  tgpmulg  24133  tsmssplit  24192  xblss2ps  24441  xblss2  24442  metustfbas  24597  nmoix  24769  nmoleub  24771  idnghm  24783  blcvx  24838  icccmp  24866  xrge0tsms  24875  metdstri  24892  nmoleub2lem  25156  rrxcph  25434  rrxdstprj1  25451  ivthle  25498  ivthle2  25499  dyadmbl  25642  volivth  25649  itg2const2  25783  itg2mulc  25789  dvlip2  26037  dvfsumlem1  26068  mdegmullem  26118  coemulhi  26294  dgrcolem2  26314  coseq00topi  26544  abssinper  26563  cxplea  26738  cxple2  26739  cxple2a  26741  cxpcn3  26790  cxpaddlelem  26793  cxpaddle  26794  ang180lem3  26853  dcubic2  26886  birthdaylem2  26994  jensen  27030  ppiltx  27218  chtub  27253  bcmono  27318  bcmax  27319  bpos  27334  lgseisenlem1  27416  2sqlem4  27462  2sqmod  27477  pntrlog2bndlem5  27622  pntpbnd1  27627  noinfbnd2lem1  27771  noetasuplem4  27777  noetainflem4  27781  mulsproplem12  28197  mulsproplem13  28198  mulsproplem14  28199  lemulsd  28208  mulsge0d  28216  mulscan2d  28249  lemuls1ad  28252  absmuls  28314  absnegs  28317  leabss  28318  tgldimor  28648  tgifscgr  28654  tgcgrxfr  28664  tgbtwnconn1  28721  tgbtwnconn2  28722  tgbtwnconn3  28723  tgbtwnconnln3  28724  tgbtwnconn22  28725  tgbtwnconnln1  28726  tgbtwnconnln2  28727  legtrid  28737  legbtwn  28740  tgcgrsub2  28741  legov3  28744  hlln  28753  hltr  28756  btwnhl  28760  ncolncol  28792  mirconn  28824  krippen  28837  midexlem  28838  midex  28883  opphllem2  28894  opphllem5  28897  opphllem6  28898  outpasch  28901  hlpasch  28902  trgcopyeulem  28951  cgrahl  28973  cgracol  28974  ex-natded5.7  30559  ex-natded5.13  30563  ex-natded9.20  30565  ex-natded9.20-2  30566  fconst7v  32772  suppovss  32833  nn0mnfxrd  32903  xrge0infss  32912  xnn0gt0  32921  nn0xmulclb  32923  difioo  32934  iundisjcnt  32950  f1ocnt  32952  fzo0opth  32955  hashxpe  32959  sgncl  32983  sgnmul  32987  nexple  32996  2exple2exp  32997  ccatws1f1o  33090  xrsmulgzz  33148  xrge0addgt0  33156  xrge0adddir  33157  ressmulgnn0d  33185  xrge0tsmsd  33214  gsumwun  33217  tocyc01  33259  cycpmco2lem4  33270  cycpmco2lem7  33273  cycpmco2  33274  cyc3co2  33281  cycpmrn  33284  archirngz  33330  archiabllem2a  33335  elrgspnlem2  33385  ssdifidllem  33604  ssmxidllem  33622  rprmirred  33688  rprmdvdspow  33690  1arithufdlem3  33703  dfufd2lem  33706  ply1dg3rt0irred  33741  esplyfval1  33831  lindsun  33883  lbsdiflsp0  33884  fldextrspunlsplem  33931  constrmon  34002  constrconj  34003  constrfin  34004  constrelextdg2  34005  constrextdg2lem  34006  zconstr  34022  submateq  34067  lmat22lem  34075  locfinref  34099  xrge0mulc1cn  34199  zrhcntr  34237  qqhval2lem  34239  esumpcvgval  34336  esumcvg  34344  sigaclcu3  34380  measiuns  34475  voliune  34487  volfiniune  34488  volmeas  34489  gsumnunsn  34799  signsply0  34809  signswch  34819  signslema  34820  signstfvneq0  34830  chtvalz  34887  btwnlng13  34928  bnj517  35144  bnj1408  35295  bnj1423  35310  bnj1452  35311  weiunse  36792  dnibndlem13  36892  dnibnd  36893  irrdifflemf  37781  poimirlem2  38085  fdc  38208  orel  38565  lsatcvat  39638  lkrpssN  39751  2at0mat0  40113  atmod1i1m  40446  lhp2at0nle  40623  trlcone  41316  tendoex  41563  dihlspsnssN  41920  dochkrsm  42046  lcfl8  42090  lclkrlem2b  42096  lclkrlem2s  42113  lcfrlem21  42151  mapdval2N  42218  mapdspex  42256  aks4d1p5  42661  hashnexinjle  42710  sticksstones12a  42738  sticksstones13  42740  sn-msqgt0d  43072  fimgmcyclem  43115  fsuppind  43136  flt4lem7  43205  nna4b4nsq  43206  pell1qrgaplem  43414  monotoddzzfi  43483  oddcomabszz  43485  zindbi  43487  rmxnn  43492  jm2.24  43504  acongeq  43524  jm2.23  43537  jm2.26lem3  43542  wepwsolem  43583  oe0rif  43826  onmcl  43872  omabs2  43873  omcl2  43874  onsucunipr  43913  oaun3lem1  43915  fzuntgd  43998  frege102d  44294  fnchoice  45573  refsum2cnlem1  45581  wallispilem3  46605  chnsubseqwl  47419  squeezedltsq  47428  wtgoldbnnsum4prm  48388  bgoldbnnsum3prm  48390  nn0sumshdiglem1  49207  mofeu  49433  toslat  49567  2arwcatlem2  50181  2arwcatlem3  50182  2arwcatlem4  50183  2arwcatlem5  50184  2arwcat  50185