Theorem mpjaodan 803

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1341  dcun  3602  ifcldadc  3633  ifeq1dadc  3634  ifeq2dadc  3635  ifeqdadc  3636  ifbothdadc  3637  ifcldcd  3641  2if2dc  3643  exmidn0m  4289  exmidsssn  4290  exmidundif  4294  exmidundifim  4295  ordtri2or2exmidlem  4622  reg2exmidlema  4630  nnpredcl  4719  frecabcl  6560  nnsucuniel  6658  dcdifsnid  6667  pw2f1odclem  7015  phpm  7047  fidifsnen  7052  dif1enen  7064  fin0  7069  fimax2gtrilemstep  7085  finexdc  7087  elssdc  7089  eqsndc  7090  en2eqpr  7094  fientri3  7102  unsnfidcex  7107  unsnfidcel  7108  undifdcss  7110  prfidceq  7115  tpfidceq  7117  fiintim  7118  ssfirab  7123  fidcenumlemrks  7146  fidcenumlemr  7148  omp1eomlem  7287  difinfsnlem  7292  difinfsn  7293  ctssdccl  7304  ctssdc  7306  enumct  7308  nninfninc  7316  nnnninf  7319  nnnninfeq  7321  nnnninfeq2  7322  nninfisol  7326  finomni  7333  ismkvnex  7348  nninfwlpoimlemg  7368  pr2cv1  7394  exmidfodomrlemeldju  7403  exmidfodomrlemreseldju  7404  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  exmidaclem  7416  exmidontriimlem3  7431  netap  7466  2omotaplemap  7469  mullocprlem  7783  recexprlemloc  7844  suplocsrlem  8021  btwnapz  9603  xnn0dcle  10030  xnn0letri  10031  z2ge  10054  xaddcom  10089  xnegdi  10096  xaddass  10097  xpncan  10099  xleadd1a  10101  xsubge0  10109  xlesubadd  10111  fztri3or  10267  fzm1  10328  fzneuz  10329  exfzdc  10479  zsupcllemstep  10482  infssuzex  10486  exbtwnzlemstep  10500  rebtwn2zlemstep  10505  xqltnle  10520  apbtwnz  10527  modifeq2int  10641  modsumfzodifsn  10651  iseqf1olemab  10757  iseqf1olemmo  10760  seq3f1olemqsumk  10767  seq3f1olemqsum  10768  seq3f1olemstep  10769  seqf1oglem1  10774  seqf1oglem2  10775  fser0const  10790  expaddzaplem  10837  qsqeqor  10905  expnbnd  10918  nn0ltexp2  10964  apexp1  10973  bcval  11004  bccmpl  11009  bcval5  11018  bcpasc  11021  bccl  11022  hashennnuni  11034  hashnncl  11050  fiubm  11085  zfz1isolemiso  11096  lswex  11158  ccatsymb  11172  ccat1st1st  11211  fzowrddc  11221  swrd0g  11234  swrdsbslen  11240  swrdspsleq  11241  pfxclz  11253  pfxwrdsymbg  11264  swrdccatin1  11299  resqrexlemnm  11572  resqrexlemcvg  11573  resqrexlemoverl  11575  resqrexlemglsq  11576  leabs  11628  nn0abscl  11639  ltabs  11641  abslt  11642  fzomaxdif  11667  maxleim  11759  maxabslemval  11762  zmaxcl  11778  2zsupmax  11780  minmax  11784  2zinfmin  11797  xrmaxleim  11798  xrmaxifle  11800  xrmaxiflemab  11801  xrmaxiflemlub  11802  xrmaxiflemcom  11803  xrmaxiflemval  11804  xrmaxaddlem  11814  xrmaxadd  11815  xrminmax  11819  sumdc  11912  sumrbdc  11933  summodclem3  11934  summodclem2a  11935  zsumdc  11938  isumss  11945  fisumss  11946  isumss2  11947  fsumcllem  11953  fsumadd  11960  fsumsplit  11961  fsumsplitsn  11964  sumsplitdc  11986  fisumrev2  12000  fsummulc2  12002  telfsumo  12020  fsumparts  12024  cvgratnnlemseq  12080  cvgratz  12086  fproddccvg  12126  prodrbdc  12128  zproddc  12133  prod1dc  12140  fprodssdc  12144  fprodmul  12145  fprodsplitdc  12150  fprodsplit  12151  fprodunsn  12158  fprodcllem  12160  sinltxirr  12315  fsumdvds  12396  dvdsle  12398  mod2eq1n2dvds  12433  bitsmod  12510  gcdsupex  12521  gcdsupcl  12522  gcdval  12523  gcddvds  12527  gcdcl  12530  gcd0id  12543  gcdneg  12546  bezoutlemmain  12562  bezoutlemzz  12566  bezoutlemaz  12567  bezoutlembz  12568  dfgcd3  12574  dfgcd2  12578  nninfctlemfo  12604  nn0seqcvgd  12606  eucalgf  12620  eucalginv  12621  dvdslcm  12634  lcmcl  12637  lcmneg  12639  lcmgcd  12643  lcmdvds  12644  lcmid  12645  mulgcddvds  12659  isprm5lem  12706  pw2dvdslemn  12730  sqrt2irrap  12745  phibndlem  12781  prm23ge5  12830  pclemdc  12854  pcxqcl  12878  pcge0  12879  pcdvdsb  12886  pceq0  12888  pcneg  12891  pcdvdstr  12893  pcgcd1  12894  pcgcd  12895  pc2dvds  12896  pcz  12898  pcprmpw2  12899  pcaddlem  12905  pcadd  12906  pcmpt  12909  pcmpt2  12910  pcprod  12912  fldivp1  12914  qexpz  12918  1arithlem4  12932  1arith  12933  4sqlem19  12975  ennnfonelemss  13024  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ctiunctlemudc  13051  bassetsnn  13132  fvprif  13419  gsumfzz  13571  gsumwsubmcl  13572  gsumwmhm  13574  gsumfzcl  13575  mulgnn0p1  13713  mulgnn0subcl  13715  mulgsubcl  13716  mulgneg  13720  mulgz  13730  mulgnn0dir  13732  mulgdirlem  13733  mulgdir  13734  submmulg  13746  ghmmulg  13836  gsumfzreidx  13917  gsumfzsubmcl  13918  gsumfzmptfidmadd  13919  gsumfzmhm  13923  lringuplu  14203  gsumfzfsum  14595  znf1o  14658  xblss2ps  15121  xblss2  15122  qtopbas  15239  dedekindeulemeu  15339  dedekindeu  15340  suplociccreex  15341  dedekindicclemeu  15348  dedekindicclemicc  15349  limcimolemlt  15381  cnplimclemle  15385  dvmptc  15434  reeff1o  15490  efltlemlt  15491  sin0pilem2  15499  coseq0negpitopi  15553  abssinper  15563  cos02pilt1  15568  logbgcd1irraplemexp  15685  lgslem4  15725  lgsneg  15746  lgsneg1  15747  lgsmod  15748  lgsdilem  15749  lgsdir2  15755  lgsdirprm  15756  lgsdir  15757  lgsdi  15759  lgsne0  15760  lgsdirnn0  15769  lgsdinn0  15770  gausslemma2dlem1a  15780  gausslemma2dlem1f1o  15782  gausslemma2dlem4  15786  lgseisenlem1  15792  lgsquad3  15806  2sqlem4  15840  2sqlem9  15846  2omap  16544  nnsf  16557  nninfsellemsuc  16564  nnnninfex  16574  trilpolemclim  16590  trilpolemisumle  16592  trilpolemeq1  16594  trilpolemlt1  16595  trirec0  16598  apdifflemf  16600  apdifflemr  16601  apdiff  16602  iswomni0  16605  nconstwlpolemgt0  16618  nconstwlpolem  16619  neapmkvlem  16621  gfsumval  16630  gsumgfsum  16634