Theorem mpjaodan 800

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 799	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
5	1, 4	mpdan 421	1 ⊢ (𝜑 → 𝜒)

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

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1320  dcun  3572  ifcldadc  3602  ifeq1dadc  3603  ifeq2dadc  3604  ifeqdadc  3605  ifbothdadc  3606  ifcldcd  3610  exmidn0m  4250  exmidsssn  4251  exmidundif  4255  exmidundifim  4256  ordtri2or2exmidlem  4579  reg2exmidlema  4587  nnpredcl  4676  frecabcl  6495  nnsucuniel  6591  dcdifsnid  6600  pw2f1odclem  6943  phpm  6974  fidifsnen  6979  dif1enen  6989  fin0  6994  fimax2gtrilemstep  7009  finexdc  7011  en2eqpr  7016  fientri3  7024  unsnfidcex  7029  unsnfidcel  7030  undifdcss  7032  prfidceq  7037  tpfidceq  7039  fiintim  7040  ssfirab  7045  fidcenumlemrks  7067  fidcenumlemr  7069  omp1eomlem  7208  difinfsnlem  7213  difinfsn  7214  ctssdccl  7225  ctssdc  7227  enumct  7229  nninfninc  7237  nnnninf  7240  nnnninfeq  7242  nnnninfeq2  7243  nninfisol  7247  finomni  7254  ismkvnex  7269  nninfwlpoimlemg  7289  exmidfodomrlemeldju  7320  exmidfodomrlemreseldju  7321  exmidfodomrlemr  7323  exmidfodomrlemrALT  7324  exmidaclem  7333  exmidontriimlem3  7348  netap  7379  2omotaplemap  7382  mullocprlem  7696  recexprlemloc  7757  suplocsrlem  7934  btwnapz  9516  xnn0dcle  9937  xnn0letri  9938  z2ge  9961  xaddcom  9996  xnegdi  10003  xaddass  10004  xpncan  10006  xleadd1a  10008  xsubge0  10016  xlesubadd  10018  fztri3or  10174  fzm1  10235  fzneuz  10236  exfzdc  10382  zsupcllemstep  10385  infssuzex  10389  exbtwnzlemstep  10403  rebtwn2zlemstep  10408  xqltnle  10423  apbtwnz  10430  modifeq2int  10544  modsumfzodifsn  10554  iseqf1olemab  10660  iseqf1olemmo  10663  seq3f1olemqsumk  10670  seq3f1olemqsum  10671  seq3f1olemstep  10672  seqf1oglem1  10677  seqf1oglem2  10678  fser0const  10693  expaddzaplem  10740  qsqeqor  10808  expnbnd  10821  nn0ltexp2  10867  apexp1  10876  bcval  10907  bccmpl  10912  bcval5  10921  bcpasc  10924  bccl  10925  hashennnuni  10937  hashnncl  10953  fiubm  10986  zfz1isolemiso  10997  lswex  11058  ccatsymb  11072  ccat1st1st  11107  fzowrddc  11114  swrd0g  11127  swrdsbslen  11133  swrdspsleq  11134  pfxwrdsymbg  11155  resqrexlemnm  11379  resqrexlemcvg  11380  resqrexlemoverl  11382  resqrexlemglsq  11383  leabs  11435  nn0abscl  11446  ltabs  11448  abslt  11449  fzomaxdif  11474  maxleim  11566  maxabslemval  11569  zmaxcl  11585  2zsupmax  11587  minmax  11591  2zinfmin  11604  xrmaxleim  11605  xrmaxifle  11607  xrmaxiflemab  11608  xrmaxiflemlub  11609  xrmaxiflemcom  11610  xrmaxiflemval  11611  xrmaxaddlem  11621  xrmaxadd  11622  xrminmax  11626  sumdc  11719  sumrbdc  11740  summodclem3  11741  summodclem2a  11742  zsumdc  11745  isumss  11752  fisumss  11753  isumss2  11754  fsumcllem  11760  fsumadd  11767  fsumsplit  11768  fsumsplitsn  11771  sumsplitdc  11793  fisumrev2  11807  fsummulc2  11809  telfsumo  11827  fsumparts  11831  cvgratnnlemseq  11887  cvgratz  11893  fproddccvg  11933  prodrbdc  11935  zproddc  11940  prod1dc  11947  fprodssdc  11951  fprodmul  11952  fprodsplitdc  11957  fprodsplit  11958  fprodunsn  11965  fprodcllem  11967  sinltxirr  12122  fsumdvds  12203  dvdsle  12205  mod2eq1n2dvds  12240  bitsmod  12317  gcdsupex  12328  gcdsupcl  12329  gcdval  12330  gcddvds  12334  gcdcl  12337  gcd0id  12350  gcdneg  12353  bezoutlemmain  12369  bezoutlemzz  12373  bezoutlemaz  12374  bezoutlembz  12375  dfgcd3  12381  dfgcd2  12385  nninfctlemfo  12411  nn0seqcvgd  12413  eucalgf  12427  eucalginv  12428  dvdslcm  12441  lcmcl  12444  lcmneg  12446  lcmgcd  12450  lcmdvds  12451  lcmid  12452  mulgcddvds  12466  isprm5lem  12513  pw2dvdslemn  12537  sqrt2irrap  12552  phibndlem  12588  prm23ge5  12637  pclemdc  12661  pcxqcl  12685  pcge0  12686  pcdvdsb  12693  pceq0  12695  pcneg  12698  pcdvdstr  12700  pcgcd1  12701  pcgcd  12702  pc2dvds  12703  pcz  12705  pcprmpw2  12706  pcaddlem  12712  pcadd  12713  pcmpt  12716  pcmpt2  12717  pcprod  12719  fldivp1  12721  qexpz  12725  1arithlem4  12739  1arith  12740  4sqlem19  12782  ennnfonelemss  12831  ennnfonelemkh  12833  ennnfonelemhf1o  12834  ctiunctlemudc  12858  fvprif  13225  gsumfzz  13377  gsumwsubmcl  13378  gsumwmhm  13380  gsumfzcl  13381  mulgnn0p1  13519  mulgnn0subcl  13521  mulgsubcl  13522  mulgneg  13526  mulgz  13536  mulgnn0dir  13538  mulgdirlem  13539  mulgdir  13540  submmulg  13552  ghmmulg  13642  gsumfzreidx  13723  gsumfzsubmcl  13724  gsumfzmptfidmadd  13725  gsumfzmhm  13729  lringuplu  14008  gsumfzfsum  14400  znf1o  14463  xblss2ps  14926  xblss2  14927  qtopbas  15044  dedekindeulemeu  15144  dedekindeu  15145  suplociccreex  15146  dedekindicclemeu  15153  dedekindicclemicc  15154  limcimolemlt  15186  cnplimclemle  15190  dvmptc  15239  reeff1o  15295  efltlemlt  15296  sin0pilem2  15304  coseq0negpitopi  15358  abssinper  15368  cos02pilt1  15373  logbgcd1irraplemexp  15490  lgslem4  15530  lgsneg  15551  lgsneg1  15552  lgsmod  15553  lgsdilem  15554  lgsdir2  15560  lgsdirprm  15561  lgsdir  15562  lgsdi  15564  lgsne0  15565  lgsdirnn0  15574  lgsdinn0  15575  gausslemma2dlem1a  15585  gausslemma2dlem1f1o  15587  gausslemma2dlem4  15591  lgseisenlem1  15597  lgsquad3  15611  2sqlem4  15645  2sqlem9  15651  2omap  16047  nnsf  16057  nninfsellemsuc  16064  nnnninfex  16074  trilpolemclim  16090  trilpolemisumle  16092  trilpolemeq1  16094  trilpolemlt1  16095  trirec0  16098  apdifflemf  16100  apdifflemr  16101  apdiff  16102  iswomni0  16105  nconstwlpolemgt0  16118  nconstwlpolem  16119  neapmkvlem  16121