Theorem mpjaodan 973

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30891. (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 700	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  onunel  6469  weniso  7361  isf32lem2  10360  isf32lem4  10362  fpwwe2lem10  10653  fpwwe2lem11  10654  lecasei  11344  ltlecasei  11346  xaddass  13305  xlesubadd  13319  xmulge0  13340  xadddi2  13353  xrsupss  13365  xrinfmss  13366  fzm1  13666  seqf1olem2  14110  expaddzlem  14173  discr  14308  sgncl  15174  sgnmul  15184  fzomaxdif  15435  iseralt  15776  sumrb  15803  telfsumo  15893  fsumparts  15897  ntrivcvgtail  15993  prodrb  16025  bitsf1  16542  smupvallem  16579  eucalgf  16679  eucalginv  16680  vdwmc2  17077  fvprif  17653  mreexmrid  17737  mreexexlem3d  17740  chnub  18716  chnccats1  18719  chnccat  18720  mulgfval  19198  ressmulgnn0  19206  mulgnn0p1  19214  mulgnn0subcl  19216  mulgsubcl  19217  mulgneg  19221  mulgz  19231  mulgnn0dir  19233  mulgdirlem  19234  mulgdir  19235  submmulg  19247  ghmmulg  19361  odid  19671  oddvds  19680  dfod2  19697  gexid  19714  gexdvds  19717  mulgnn0di  19958  mulgdi  19959  gsumzsplit  20060  2nsgsimpgd  20237  prmgrpsimpgd  20249  lringuplu  20712  lsppratlem5  21344  ssdifidllem  21553  prmirred  21693  mhpmulcl  22383  1stckgenlem  23785  qtoprest  23949  tgpmulg  24325  tsmssplit  24384  xblss2ps  24633  xblss2  24634  metustfbas  24789  nmoix  24961  nmoleub  24963  idnghm  24975  blcvx  25030  icccmp  25058  xrge0tsms  25067  metdstri  25084  nmoleub2lem  25348  rrxcph  25626  rrxdstprj1  25643  ivthle  25690  ivthle2  25691  dyadmbl  25834  volivth  25841  itg2const2  25975  itg2mulc  25981  dvlip2  26229  dvfsumlem1  26260  mdegmullem  26310  coemulhi  26487  dgrcolem2  26507  coseq00topi  26747  abssinper  26766  cxplea  26941  cxple2  26942  cxple2a  26944  cxpcn3  26993  cxpaddlelem  26996  cxpaddle  26997  ang180lem3  27056  dcubic2  27089  birthdaylem2  27197  jensen  27233  ppiltx  27421  chtub  27456  bcmono  27521  bcmax  27522  bpos  27537  lgseisenlem1  27619  2sqlem4  27665  2sqmod  27680  pntrlog2bndlem5  27825  pntpbnd1  27830  noinfbnd2lem1  27974  noetasuplem4  27980  noetainflem4  27984  mulsproplem12  28400  mulsproplem13  28401  mulsproplem14  28402  lemulsd  28411  mulsge0d  28419  mulscan2d  28452  lemuls1ad  28455  absmuls  28517  absnegs  28520  leabss  28521  tgldimor  28852  tgifscgr  28858  tgcgrxfr  28868  tgbtwnconn1  28925  tgbtwnconn2  28926  tgbtwnconn3  28927  tgbtwnconnln3  28928  tgbtwnconn22  28929  tgbtwnconnln1  28930  tgbtwnconnln2  28931  legtrid  28941  legbtwn  28944  tgcgrsub2  28945  legov3  28948  hlln  28960  hltr  28963  btwnhl  28967  ncolncol  29002  mirconn  29037  krippen  29050  midexlem  29051  midex  29100  opphllem2  29111  opphllem5  29114  opphllem6  29115  outpasch  29120  hlpasch  29121  plngcplem  29150  plngrotlem1  29152  plngrotlem2  29153  lnssplng  29157  trgcopyeulem  29199  cgrahl  29222  cgracol  29223  tgaaddcpbllem3  29238  tgaaddcpbl2  29240  angmgmaddov1lem  29273  angmgmaddov2lem  29274  angmgmaddcpbl  29277  angmgmaddcl  29278  angmgmaddrid  29280  prlngmolem2  29318  ex-natded5.7  30899  ex-natded5.13  30903  ex-natded9.20  30905  ex-natded9.20-2  30906  fconst7v  33101  suppovss  33161  nn0mnfxrd  33230  xrge0infss  33239  xnn0gt0  33248  nn0xmulclb  33250  difioo  33261  iundisjcnt  33277  f1ocnt  33279  fzo0opth  33282  hashxpe  33286  nexple  33311  2exple2exp  33312  ccatws1f1o  33401  xrsmulgzz  33457  xrge0addgt0  33465  xrge0adddir  33466  ressmulgnn0d  33492  xrge0tsmsd  33521  gsumwun  33524  tocyc01  33566  cycpmco2lem4  33577  cycpmco2lem7  33580  cycpmco2  33581  cyc3co2  33588  cycpmrn  33591  archirngz  33637  archiabllem2a  33642  elrgspnlem2  33691  ssmxidllem  33884  rprmirred  33949  rprmdvdspow  33951  1arithufdlem3  33964  dfufd2lem  33967  ply1dg3rt0irred  34002  esplyfval1  34091  lindsun  34143  lbsdiflsp0  34144  fldextrspunlsplem  34191  constrmon  34262  constrconj  34263  constrfin  34264  constrelextdg2  34265  constrextdg2lem  34266  zconstr  34282  submateq  34327  lmat22lem  34335  locfinref  34359  xrge0mulc1cn  34459  zrhcntr  34497  qqhval2lem  34499  esumpcvgval  34596  esumcvg  34604  sigaclcu3  34640  measiuns  34736  voliune  34748  volfiniune  34749  volmeas  34750  gsumnunsn  35060  signsply0  35067  signswch  35077  signslema  35078  signstfvneq0  35088  chtvalz  35145  btwnlng13  35186  bnj517  35402  bnj1408  35553  bnj1423  35568  bnj1452  35569  weiunse  37095  dnibndlem13  37195  dnibnd  37196  irrdifflemf  38085  poimirlem2  38379  fdc  38503  orel  38858  lsatcvat  39931  lkrpssN  40044  2at0mat0  40406  atmod1i1m  40739  lhp2at0nle  40916  trlcone  41609  tendoex  41856  dihlspsnssN  42213  dochkrsm  42339  lcfl8  42383  lclkrlem2b  42389  lclkrlem2s  42406  lcfrlem21  42444  mapdval2N  42511  mapdspex  42549  aks4d1p5  42954  hashnexinjle  43003  sticksstones12a  43031  sticksstones13  43033  sn-msqgt0d  43382  fimgmcyclem  43423  fsuppind  43444  flt4lem7  43513  nna4b4nsq  43514  pell1qrgaplem  43722  monotoddzzfi  43791  oddcomabszz  43793  zindbi  43795  rmxnn  43800  jm2.24  43812  acongeq  43832  jm2.23  43845  jm2.26lem3  43850  wepwsolem  43891  oe0rif  44134  onmcl  44180  omabs2  44181  omcl2  44182  onsucunipr  44221  oaun3lem1  44223  fzuntgd  44306  frege102d  44602  fnchoice  45871  refsum2cnlem1  45879  wallispilem3  46903  chnsubseqwl  47715  wtgoldbnnsum4prm  48726  bgoldbnnsum3prm  48728  nn0sumshdiglem1  49559  mofeu  49784  toslat  49916  2arwcatlem2  50530  2arwcatlem3  50531  2arwcatlem4  50532  2arwcatlem5  50533  2arwcat  50534  veronesevrowd  50820