Theorem mpjaodan 973

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 31009. (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  6470  weniso  7364  isf32lem2  10435  isf32lem4  10437  fpwwe2lem10  10728  fpwwe2lem11  10729  lecasei  11419  ltlecasei  11421  xaddass  13382  xlesubadd  13396  xmulge0  13417  xadddi2  13430  xrsupss  13442  xrinfmss  13443  fzm1  13744  seqf1olem2  14188  expaddzlem  14251  discr  14387  sgncl  15255  sgnmul  15265  fzomaxdif  15516  iseralt  15857  sumrb  15884  telfsumo  15974  fsumparts  15978  ntrivcvgtail  16074  prodrb  16104  bitsf1  16621  smupvallem  16658  eucalgf  16763  eucalginv  16764  vdwmc2  17162  fvprif  17738  mreexmrid  17822  mreexexlem3d  17825  chnub  18801  chnccats1  18804  chnccat  18805  mulgfval  19284  ressmulgnn0  19292  mulgnn0p1  19300  mulgnn0subcl  19302  mulgsubcl  19303  mulgneg  19307  mulgz  19317  mulgnn0dir  19319  mulgdirlem  19320  mulgdir  19321  submmulg  19333  ghmmulg  19447  odid  19757  oddvds  19766  dfod2  19783  gexid  19800  gexdvds  19803  mulgnn0di  20044  mulgdi  20045  gsumzsplit  20146  2nsgsimpgd  20323  prmgrpsimpgd  20335  lringuplu  20801  lsppratlem5  21434  ssdifidllem  21645  prmirred  21785  mhpmulcl  22475  1stckgenlem  23877  qtoprest  24041  tgpmulg  24417  tsmssplit  24476  xblss2ps  24725  xblss2  24726  metustfbas  24881  nmoix  25053  nmoleub  25055  idnghm  25067  blcvx  25122  icccmp  25150  xrge0tsms  25159  metdstri  25176  nmoleub2lem  25440  rrxcph  25718  rrxdstprj1  25735  ivthle  25782  ivthle2  25783  dyadmbl  25926  volivth  25933  itg2const2  26067  itg2mulc  26073  dvlip2  26320  dvfsumlem1  26351  mdegmullem  26401  coemulhi  26578  dgrcolem2  26598  coseq00topi  26836  abssinper  26854  cxplea  27029  cxple2  27030  cxple2a  27032  cxpcn3  27081  cxpaddlelem  27084  cxpaddle  27085  ang180lem3  27144  dcubic2  27177  birthdaylem2  27285  jensen  27321  ppiltx  27509  chtub  27544  bcmono  27609  bcmax  27610  bpos  27625  lgseisenlem1  27707  2sqlem4  27753  2sqmod  27768  pntrlog2bndlem5  27913  pntpbnd1  27918  flt4lem7  27994  nna4b4nsq  27995  noinfbnd2lem1  28092  noetasuplem4  28098  noetainflem4  28102  mulsproplem12  28518  mulsproplem13  28519  mulsproplem14  28520  lemulsd  28529  mulsge0d  28537  mulscan2d  28570  lemuls1ad  28573  absmuls  28635  absnegs  28638  leabss  28639  tgldimor  28970  tgifscgr  28976  tgcgrxfr  28986  tgbtwnconn1  29043  tgbtwnconn2  29044  tgbtwnconn3  29045  tgbtwnconnln3  29046  tgbtwnconn22  29047  tgbtwnconnln1  29048  tgbtwnconnln2  29049  legtrid  29059  legbtwn  29062  tgcgrsub2  29063  legov3  29066  hlln  29078  hltr  29081  btwnhl  29085  ncolncol  29120  mirconn  29155  krippen  29168  midexlem  29169  midex  29218  opphllem2  29229  opphllem5  29232  opphllem6  29233  outpasch  29238  hlpasch  29239  plngcplem  29268  plngrotlem1  29270  plngrotlem2  29271  lnssplng  29275  trgcopyeulem  29317  cgrahl  29340  cgracol  29341  tgaaddcpbllem3  29356  tgaaddcpbl2  29358  angmgmaddov1lem  29391  angmgmaddov2lem  29392  angmgmaddcpbl  29395  angmgmaddcl  29396  angmgmaddrid  29398  prlngmolem2  29436  ex-natded5.7  31017  ex-natded5.13  31021  ex-natded9.20  31023  ex-natded9.20-2  31024  inagbtwn  33053  inagcgratrgn  33063  cgrainag  33065  tgextahpl  33074  tgextahp  33078  tgaasne  33087  fconst7v  33261  suppovss  33321  nn0mnfxrd  33389  xrge0infss  33398  xnn0gt0  33407  nn0xmulclb  33409  difioo  33420  iundisjcnt  33436  f1ocnt  33438  fzo0opth  33441  hashxpe  33445  nexple  33470  2exple2exp  33471  ccatws1f1o  33560  xrsmulgzz  33616  xrge0addgt0  33624  xrge0adddir  33625  ressmulgnn0d  33651  xrge0tsmsd  33680  gsumwun  33683  tocyc01  33725  cycpmco2lem4  33736  cycpmco2lem7  33739  cycpmco2  33740  cyc3co2  33747  cycpmrn  33750  archirngz  33796  archiabllem2a  33801  elrgspnlem2  33850  ssmxidllem  34044  rprmirred  34109  rprmdvdspow  34111  1arithufdlem3  34124  dfufd2lem  34127  ply1dg3rt0irred  34162  esplyfval1  34251  lindsun  34303  lbsdiflsp0  34304  fldextrspunlsplem  34351  constrmon  34422  constrconj  34423  constrfin  34424  constrelextdg2  34425  constrextdg2lem  34426  zconstr  34442  submateq  34487  lmat22lem  34495  locfinref  34519  xrge0mulc1cn  34619  zrhcntr  34657  qqhval2lem  34659  esumpcvgval  34756  esumcvg  34764  sigaclcu3  34800  measiuns  34896  voliune  34908  volfiniune  34909  volmeas  34910  gsumnunsn  35219  signsply0  35226  signswch  35236  signslema  35237  signstfvneq0  35247  chtvalz  35304  btwnlng13  35345  bnj517  35561  bnj1408  35712  bnj1423  35727  bnj1452  35728  weiunse  37348  dnibndlem13  37448  dnibnd  37449  irrdifflemf  38339  poimirlem2  38633  fdc  38772  orel  39127  lsatcvat  40200  lkrpssN  40313  2at0mat0  40675  atmod1i1m  41008  lhp2at0nle  41185  trlcone  41878  tendoex  42125  dihlspsnssN  42482  dochkrsm  42608  lcfl8  42652  lclkrlem2b  42658  lclkrlem2s  42675  lcfrlem21  42713  mapdval2N  42780  mapdspex  42818  aks4d1p5  43223  hashnexinjle  43272  sticksstones12a  43300  sticksstones13  43302  sn-msqgt0d  43643  fimgmcyclem  43690  fsuppind  43711  pell1qrgaplem  43973  monotoddzzfi  44042  oddcomabszz  44044  zindbi  44046  rmxnn  44051  jm2.24  44063  acongeq  44083  jm2.23  44096  jm2.26lem3  44101  wepwsolem  44142  oe0rif  44380  onmcl  44426  omabs2  44427  omcl2  44428  onsucunipr  44467  oaun3lem1  44469  fzuntgd  44552  frege102d  44847  fnchoice  46139  refsum2cnlem1  46147  wallispilem3  47170  chnsubseqwl  47982  wtgoldbnnsum4prm  48993  bgoldbnnsum3prm  48995  nn0sumshdiglem1  49826  mofeu  50052  toslat  50189  2arwcatlem2  50827  2arwcatlem3  50828  2arwcatlem4  50829  2arwcatlem5  50830  2arwcat  50831  parhomco2  50853  parhomco  50854  parmapco2  50865  parmapco  50866  veronesevrowd  51147