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	|- ( ( ph /\ ps ) -> ch )
jaodan.2	|- ( ( ph /\ th ) -> ch )
jaodan.3	|- ( ph -> ( ps \/ th ) )

Assertion

Ref	Expression
mpjaodan	|- ( ph -> ch )

Proof of Theorem mpjaodan

Step	Hyp	Ref	Expression
1		jaodan.3	. 2 |- ( ph -> ( ps \/ th ) )
2		jaodan.1	. . 3 |- ( ( ph /\ ps ) -> ch )
3		jaodan.2	. . 3 |- ( ( ph /\ th ) -> ch )
4	2, 3	jaodan 802	. 2 |- ( ( ph /\ ( ps \/ th ) ) -> ch )
5	1, 4	mpdan 421	1 |- ( ph -> ch )

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  3601  ifcldadc  3632  ifeq1dadc  3633  ifeq2dadc  3634  ifeqdadc  3635  ifbothdadc  3636  ifcldcd  3640  2if2dc  3642  exmidn0m  4285  exmidsssn  4286  exmidundif  4290  exmidundifim  4291  ordtri2or2exmidlem  4618  reg2exmidlema  4626  nnpredcl  4715  frecabcl  6545  nnsucuniel  6641  dcdifsnid  6650  pw2f1odclem  6995  phpm  7027  fidifsnen  7032  dif1enen  7042  fin0  7047  fimax2gtrilemstep  7062  finexdc  7064  en2eqpr  7069  fientri3  7077  unsnfidcex  7082  unsnfidcel  7083  undifdcss  7085  prfidceq  7090  tpfidceq  7092  fiintim  7093  ssfirab  7098  fidcenumlemrks  7120  fidcenumlemr  7122  omp1eomlem  7261  difinfsnlem  7266  difinfsn  7267  ctssdccl  7278  ctssdc  7280  enumct  7282  nninfninc  7290  nnnninf  7293  nnnninfeq  7295  nnnninfeq2  7296  nninfisol  7300  finomni  7307  ismkvnex  7322  nninfwlpoimlemg  7342  pr2cv1  7368  exmidfodomrlemeldju  7377  exmidfodomrlemreseldju  7378  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  exmidaclem  7390  exmidontriimlem3  7405  netap  7440  2omotaplemap  7443  mullocprlem  7757  recexprlemloc  7818  suplocsrlem  7995  btwnapz  9577  xnn0dcle  9998  xnn0letri  9999  z2ge  10022  xaddcom  10057  xnegdi  10064  xaddass  10065  xpncan  10067  xleadd1a  10069  xsubge0  10077  xlesubadd  10079  fztri3or  10235  fzm1  10296  fzneuz  10297  exfzdc  10446  zsupcllemstep  10449  infssuzex  10453  exbtwnzlemstep  10467  rebtwn2zlemstep  10472  xqltnle  10487  apbtwnz  10494  modifeq2int  10608  modsumfzodifsn  10618  iseqf1olemab  10724  iseqf1olemmo  10727  seq3f1olemqsumk  10734  seq3f1olemqsum  10735  seq3f1olemstep  10736  seqf1oglem1  10741  seqf1oglem2  10742  fser0const  10757  expaddzaplem  10804  qsqeqor  10872  expnbnd  10885  nn0ltexp2  10931  apexp1  10940  bcval  10971  bccmpl  10976  bcval5  10985  bcpasc  10988  bccl  10989  hashennnuni  11001  hashnncl  11017  fiubm  11050  zfz1isolemiso  11061  lswex  11123  ccatsymb  11137  ccat1st1st  11172  fzowrddc  11179  swrd0g  11192  swrdsbslen  11198  swrdspsleq  11199  pfxclz  11211  pfxwrdsymbg  11222  swrdccatin1  11257  resqrexlemnm  11529  resqrexlemcvg  11530  resqrexlemoverl  11532  resqrexlemglsq  11533  leabs  11585  nn0abscl  11596  ltabs  11598  abslt  11599  fzomaxdif  11624  maxleim  11716  maxabslemval  11719  zmaxcl  11735  2zsupmax  11737  minmax  11741  2zinfmin  11754  xrmaxleim  11755  xrmaxifle  11757  xrmaxiflemab  11758  xrmaxiflemlub  11759  xrmaxiflemcom  11760  xrmaxiflemval  11761  xrmaxaddlem  11771  xrmaxadd  11772  xrminmax  11776  sumdc  11869  sumrbdc  11890  summodclem3  11891  summodclem2a  11892  zsumdc  11895  isumss  11902  fisumss  11903  isumss2  11904  fsumcllem  11910  fsumadd  11917  fsumsplit  11918  fsumsplitsn  11921  sumsplitdc  11943  fisumrev2  11957  fsummulc2  11959  telfsumo  11977  fsumparts  11981  cvgratnnlemseq  12037  cvgratz  12043  fproddccvg  12083  prodrbdc  12085  zproddc  12090  prod1dc  12097  fprodssdc  12101  fprodmul  12102  fprodsplitdc  12107  fprodsplit  12108  fprodunsn  12115  fprodcllem  12117  sinltxirr  12272  fsumdvds  12353  dvdsle  12355  mod2eq1n2dvds  12390  bitsmod  12467  gcdsupex  12478  gcdsupcl  12479  gcdval  12480  gcddvds  12484  gcdcl  12487  gcd0id  12500  gcdneg  12503  bezoutlemmain  12519  bezoutlemzz  12523  bezoutlemaz  12524  bezoutlembz  12525  dfgcd3  12531  dfgcd2  12535  nninfctlemfo  12561  nn0seqcvgd  12563  eucalgf  12577  eucalginv  12578  dvdslcm  12591  lcmcl  12594  lcmneg  12596  lcmgcd  12600  lcmdvds  12601  lcmid  12602  mulgcddvds  12616  isprm5lem  12663  pw2dvdslemn  12687  sqrt2irrap  12702  phibndlem  12738  prm23ge5  12787  pclemdc  12811  pcxqcl  12835  pcge0  12836  pcdvdsb  12843  pceq0  12845  pcneg  12848  pcdvdstr  12850  pcgcd1  12851  pcgcd  12852  pc2dvds  12853  pcz  12855  pcprmpw2  12856  pcaddlem  12862  pcadd  12863  pcmpt  12866  pcmpt2  12867  pcprod  12869  fldivp1  12871  qexpz  12875  1arithlem4  12889  1arith  12890  4sqlem19  12932  ennnfonelemss  12981  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ctiunctlemudc  13008  bassetsnn  13089  fvprif  13376  gsumfzz  13528  gsumwsubmcl  13529  gsumwmhm  13531  gsumfzcl  13532  mulgnn0p1  13670  mulgnn0subcl  13672  mulgsubcl  13673  mulgneg  13677  mulgz  13687  mulgnn0dir  13689  mulgdirlem  13690  mulgdir  13691  submmulg  13703  ghmmulg  13793  gsumfzreidx  13874  gsumfzsubmcl  13875  gsumfzmptfidmadd  13876  gsumfzmhm  13880  lringuplu  14160  gsumfzfsum  14552  znf1o  14615  xblss2ps  15078  xblss2  15079  qtopbas  15196  dedekindeulemeu  15296  dedekindeu  15297  suplociccreex  15298  dedekindicclemeu  15305  dedekindicclemicc  15306  limcimolemlt  15338  cnplimclemle  15342  dvmptc  15391  reeff1o  15447  efltlemlt  15448  sin0pilem2  15456  coseq0negpitopi  15510  abssinper  15520  cos02pilt1  15525  logbgcd1irraplemexp  15642  lgslem4  15682  lgsneg  15703  lgsneg1  15704  lgsmod  15705  lgsdilem  15706  lgsdir2  15712  lgsdirprm  15713  lgsdir  15714  lgsdi  15716  lgsne0  15717  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem1a  15737  gausslemma2dlem1f1o  15739  gausslemma2dlem4  15743  lgseisenlem1  15749  lgsquad3  15763  2sqlem4  15797  2sqlem9  15803  2omap  16359  nnsf  16371  nninfsellemsuc  16378  nnnninfex  16388  trilpolemclim  16404  trilpolemisumle  16406  trilpolemeq1  16408  trilpolemlt1  16409  trirec0  16412  apdifflemf  16414  apdifflemr  16415  apdiff  16416  iswomni0  16419  nconstwlpolemgt0  16432  nconstwlpolem  16433  neapmkvlem  16435