Theorem mpjaodan 973

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30986. (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  6463  weniso  7356  isf32lem2  10413  isf32lem4  10415  fpwwe2lem10  10706  fpwwe2lem11  10707  lecasei  11397  ltlecasei  11399  xaddass  13360  xlesubadd  13374  xmulge0  13395  xadddi2  13408  xrsupss  13420  xrinfmss  13421  fzm1  13721  seqf1olem2  14165  expaddzlem  14228  discr  14364  sgncl  15230  sgnmul  15240  fzomaxdif  15491  iseralt  15832  sumrb  15859  telfsumo  15949  fsumparts  15953  ntrivcvgtail  16049  prodrb  16079  bitsf1  16596  smupvallem  16633  eucalgf  16738  eucalginv  16739  vdwmc2  17137  fvprif  17713  mreexmrid  17797  mreexexlem3d  17800  chnub  18776  chnccats1  18779  chnccat  18780  mulgfval  19259  ressmulgnn0  19267  mulgnn0p1  19275  mulgnn0subcl  19277  mulgsubcl  19278  mulgneg  19282  mulgz  19292  mulgnn0dir  19294  mulgdirlem  19295  mulgdir  19296  submmulg  19308  ghmmulg  19422  odid  19732  oddvds  19741  dfod2  19758  gexid  19775  gexdvds  19778  mulgnn0di  20019  mulgdi  20020  gsumzsplit  20121  2nsgsimpgd  20298  prmgrpsimpgd  20310  lringuplu  20776  lsppratlem5  21409  ssdifidllem  21620  prmirred  21760  mhpmulcl  22450  1stckgenlem  23852  qtoprest  24016  tgpmulg  24392  tsmssplit  24451  xblss2ps  24700  xblss2  24701  metustfbas  24856  nmoix  25028  nmoleub  25030  idnghm  25042  blcvx  25097  icccmp  25125  xrge0tsms  25134  metdstri  25151  nmoleub2lem  25415  rrxcph  25693  rrxdstprj1  25710  ivthle  25757  ivthle2  25758  dyadmbl  25901  volivth  25908  itg2const2  26042  itg2mulc  26048  dvlip2  26295  dvfsumlem1  26326  mdegmullem  26376  coemulhi  26553  dgrcolem2  26573  coseq00topi  26813  abssinper  26831  cxplea  27006  cxple2  27007  cxple2a  27009  cxpcn3  27058  cxpaddlelem  27061  cxpaddle  27062  ang180lem3  27121  dcubic2  27154  birthdaylem2  27262  jensen  27298  ppiltx  27486  chtub  27521  bcmono  27586  bcmax  27587  bpos  27602  lgseisenlem1  27684  2sqlem4  27730  2sqmod  27745  pntrlog2bndlem5  27890  pntpbnd1  27895  flt4lem7  27971  nna4b4nsq  27972  noinfbnd2lem1  28069  noetasuplem4  28075  noetainflem4  28079  mulsproplem12  28495  mulsproplem13  28496  mulsproplem14  28497  lemulsd  28506  mulsge0d  28514  mulscan2d  28547  lemuls1ad  28550  absmuls  28612  absnegs  28615  leabss  28616  tgldimor  28947  tgifscgr  28953  tgcgrxfr  28963  tgbtwnconn1  29020  tgbtwnconn2  29021  tgbtwnconn3  29022  tgbtwnconnln3  29023  tgbtwnconn22  29024  tgbtwnconnln1  29025  tgbtwnconnln2  29026  legtrid  29036  legbtwn  29039  tgcgrsub2  29040  legov3  29043  hlln  29055  hltr  29058  btwnhl  29062  ncolncol  29097  mirconn  29132  krippen  29145  midexlem  29146  midex  29195  opphllem2  29206  opphllem5  29209  opphllem6  29210  outpasch  29215  hlpasch  29216  plngcplem  29245  plngrotlem1  29247  plngrotlem2  29248  lnssplng  29252  trgcopyeulem  29294  cgrahl  29317  cgracol  29318  tgaaddcpbllem3  29333  tgaaddcpbl2  29335  angmgmaddov1lem  29368  angmgmaddov2lem  29369  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmaddrid  29375  prlngmolem2  29413  ex-natded5.7  30994  ex-natded5.13  30998  ex-natded9.20  31000  ex-natded9.20-2  31001  fconst7v  33196  suppovss  33256  nn0mnfxrd  33325  xrge0infss  33334  xnn0gt0  33343  nn0xmulclb  33345  difioo  33356  iundisjcnt  33372  f1ocnt  33374  fzo0opth  33377  hashxpe  33381  nexple  33406  2exple2exp  33407  ccatws1f1o  33496  xrsmulgzz  33552  xrge0addgt0  33560  xrge0adddir  33561  ressmulgnn0d  33587  xrge0tsmsd  33616  gsumwun  33619  tocyc01  33661  cycpmco2lem4  33672  cycpmco2lem7  33675  cycpmco2  33676  cyc3co2  33683  cycpmrn  33686  archirngz  33732  archiabllem2a  33737  elrgspnlem2  33786  ssmxidllem  33980  rprmirred  34045  rprmdvdspow  34047  1arithufdlem3  34060  dfufd2lem  34063  ply1dg3rt0irred  34098  esplyfval1  34187  lindsun  34239  lbsdiflsp0  34240  fldextrspunlsplem  34287  constrmon  34358  constrconj  34359  constrfin  34360  constrelextdg2  34361  constrextdg2lem  34362  zconstr  34378  submateq  34423  lmat22lem  34431  locfinref  34455  xrge0mulc1cn  34555  zrhcntr  34593  qqhval2lem  34595  esumpcvgval  34692  esumcvg  34700  sigaclcu3  34736  measiuns  34832  voliune  34844  volfiniune  34845  volmeas  34846  gsumnunsn  35156  signsply0  35163  signswch  35173  signslema  35174  signstfvneq0  35184  chtvalz  35241  btwnlng13  35282  bnj517  35498  bnj1408  35649  bnj1423  35664  bnj1452  35665  weiunse  37226  dnibndlem13  37326  dnibnd  37327  irrdifflemf  38214  poimirlem2  38508  fdc  38647  orel  39002  lsatcvat  40075  lkrpssN  40188  2at0mat0  40550  atmod1i1m  40883  lhp2at0nle  41060  trlcone  41753  tendoex  42000  dihlspsnssN  42357  dochkrsm  42483  lcfl8  42527  lclkrlem2b  42533  lclkrlem2s  42550  lcfrlem21  42588  mapdval2N  42655  mapdspex  42693  aks4d1p5  43098  hashnexinjle  43147  sticksstones12a  43175  sticksstones13  43177  sn-msqgt0d  43518  fimgmcyclem  43559  fsuppind  43580  pell1qrgaplem  43833  monotoddzzfi  43902  oddcomabszz  43904  zindbi  43906  rmxnn  43911  jm2.24  43923  acongeq  43943  jm2.23  43956  jm2.26lem3  43961  wepwsolem  44002  oe0rif  44245  onmcl  44291  omabs2  44292  omcl2  44293  onsucunipr  44332  oaun3lem1  44334  fzuntgd  44417  frege102d  44713  fnchoice  45989  refsum2cnlem1  45997  wallispilem3  47021  chnsubseqwl  47833  wtgoldbnnsum4prm  48844  bgoldbnnsum3prm  48846  nn0sumshdiglem1  49677  mofeu  49902  toslat  50034  2arwcatlem2  50648  2arwcatlem3  50649  2arwcatlem4  50650  2arwcatlem5  50651  2arwcat  50652  veronesevrowd  50923