Theorem mpjaodan 806

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 805	. 2 |- ( ( ph /\ ( ps \/ th ) ) -> ch )
5	1, 4	mpdan 421	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1344  dcun  3623  ifcldadc  3656  ifeq1dadc  3657  ifeq2dadc  3658  ifeqdadc  3659  ifbothdadc  3660  ifcldcd  3664  2if2dc  3666  ifeqeqxdc  3673  exmidn0m  4319  exmidsssn  4320  exmidundif  4324  exmidundifim  4325  ordtri2or2exmidlem  4653  reg2exmidlema  4661  nnpredcl  4750  frecabcl  6643  nnsucuniel  6741  dcdifsnid  6750  pw2f1odclem  7100  phpm  7133  fidifsnen  7138  dif1enen  7150  fin0  7155  fimax2gtrilemstep  7171  finexdc  7173  elssdc  7175  eqsndc  7176  en2eqpr  7180  fientri3  7188  unsnfidcex  7193  unsnfidcel  7194  undifdcss  7196  prfidceq  7201  tpfidceq  7203  fiintim  7204  ssfirab  7210  fidcenumlemrks  7236  fidcenumlemr  7238  2omap  7282  omp1eomlem  7398  difinfsnlem  7403  difinfsn  7404  ctssdccl  7415  ctssdc  7417  enumct  7419  nninfninc  7427  nnnninf  7430  nnnninfeq  7432  nnnninfeq2  7433  nninfisol  7437  finomni  7444  ismkvnex  7459  nninfwlpoimlemg  7479  pr2cv1  7505  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  exmidontriimlem3  7543  netap  7584  2omotaplemap  7587  mullocprlem  7901  recexprlemloc  7962  suplocsrlem  8139  btwnapz  9726  xnn0dcle  10154  xnn0letri  10155  z2ge  10178  xaddcom  10213  xnegdi  10220  xaddass  10221  xpncan  10223  xleadd1a  10225  xsubge0  10233  xlesubadd  10235  fztri3or  10393  fzm1  10456  fzneuz  10457  exfzdc  10608  zsupcllemstep  10611  infssuzex  10615  exbtwnzlemstep  10631  rebtwn2zlemstep  10636  xqltnle  10651  apbtwnz  10658  modifeq2int  10772  modsumfzodifsn  10782  iseqf1olemab  10888  iseqf1olemmo  10891  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seq3f1olemstep  10900  seqf1oglem1  10905  seqf1oglem2  10906  fser0const  10921  expaddzaplem  10968  qsqeqor  11036  resq01  11044  expnbnd  11050  nn0ltexp2  11096  apexp1  11105  bcval  11136  bccmpl  11141  bcval5  11150  bcpasc  11153  bccl  11154  hashennnuni  11167  hashnncl  11183  fiubm  11220  hashfibc  11232  zfz1isolemiso  11236  lswex  11301  ccatsymb  11315  ccat1st1st  11354  fzowrddc  11364  swrd0g  11377  swrdsbslen  11383  swrdspsleq  11384  pfxclz  11396  pfxwrdsymbg  11407  swrdccatin1  11442  resqrexlemnm  11728  resqrexlemcvg  11729  resqrexlemoverl  11731  resqrexlemglsq  11732  leabs  11784  nn0abscl  11795  ltabs  11797  abslt  11798  fzomaxdif  11823  maxleim  11915  maxabslemval  11918  zmaxcl  11934  2zsupmax  11936  minmax  11940  2zinfmin  11953  xrmaxleim  11954  xrmaxifle  11956  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxiflemcom  11959  xrmaxiflemval  11960  xrmaxaddlem  11970  xrmaxadd  11971  xrminmax  11975  sumdc  12068  fzf1o  12086  sumrbdc  12090  summodclem3  12091  summodclem2a  12092  zsumdc  12095  isumss  12102  fisumss  12103  isumss2  12104  fsumcllem  12110  fsumadd  12117  fsumsplit  12118  fsumsplitsn  12121  sumsplitdc  12143  fisumrev2  12157  fsummulc2  12159  telfsumo  12177  fsumparts  12181  cvgratnnlemseq  12237  cvgratz  12243  fproddccvg  12283  prodrbdc  12285  zproddc  12290  prod1dc  12297  fprodssdc  12301  fprodmul  12302  fprodsplitdc  12307  fprodsplit  12308  fprodunsn  12315  fprodcllem  12317  sinltxirr  12472  fsumdvds  12553  dvdsle  12555  mod2eq1n2dvds  12590  bitsmod  12667  gcdsupex  12678  gcdsupcl  12679  gcdval  12680  gcddvds  12684  gcdcl  12687  gcd0id  12700  gcdneg  12703  bezoutlemmain  12719  bezoutlemzz  12723  bezoutlemaz  12724  bezoutlembz  12725  dfgcd3  12731  dfgcd2  12735  nninfctlemfo  12761  nn0seqcvgd  12763  eucalgf  12777  eucalginv  12778  dvdslcm  12791  lcmcl  12794  lcmneg  12796  lcmgcd  12800  lcmdvds  12801  lcmid  12802  mulgcddvds  12816  isprm5lem  12863  pw2dvdslemn  12887  sqrt2irrap  12902  phibndlem  12938  prm23ge5  12987  pclemdc  13011  pcxqcl  13035  pcge0  13036  pcdvdsb  13043  pceq0  13045  pcneg  13048  pcdvdstr  13050  pcgcd1  13051  pcgcd  13052  pc2dvds  13053  pcz  13055  pcprmpw2  13056  pcaddlem  13062  pcadd  13063  pcmpt  13066  pcmpt2  13067  pcprod  13069  fldivp1  13071  qexpz  13075  1arithlem4  13089  1arith  13090  4sqlem19  13132  ennnfonelemss  13245  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ctiunctlemudc  13272  bassetsnn  13353  fvprif  13607  gsumfzz  13750  gsumwsubmcl  13751  gsumwmhm  13753  gsumfzcl  13754  mulgnn0p1  13886  mulgnn0subcl  13888  mulgsubcl  13889  mulgneg  13893  mulgz  13903  mulgnn0dir  13905  mulgdirlem  13906  mulgdir  13907  submmulg  13919  ghmmulg  14009  gsumfzreidx  14090  gsumfzsubmcl  14091  gsumfzmptfidmadd  14092  gsumfzmhm  14096  gsumsplit0  14099  gfsumval  14102  gsumgfsum  14106  lringuplu  14441  aprlring  14538  gsumfzfsum  14862  znf1o  14925  xblss2ps  15395  xblss2  15396  qtopbas  15513  dedekindeulemeu  15613  dedekindeu  15614  suplociccreex  15615  dedekindicclemeu  15622  dedekindicclemicc  15623  limcimolemlt  15655  cnplimclemle  15659  dvmptc  15708  reeff1o  15764  efltlemlt  15765  sin0pilem2  15773  coseq0negpitopi  15827  abssinper  15837  cos02pilt1  15842  logbgcd1irraplemexp  15959  lgslem4  16002  lgsneg  16023  lgsneg1  16024  lgsmod  16025  lgsdilem  16026  lgsdir2  16032  lgsdirprm  16033  lgsdir  16034  lgsdi  16036  lgsne0  16037  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  gausslemma2dlem4  16063  lgseisenlem1  16069  lgsquad3  16083  2sqlem4  16117  2sqlem9  16123  eupth2lem3lem3fi  16591  eupth2lem3lem4fi  16594  eupth2lem3lem7fi  16595  nnsf  16909  nninfsellemsuc  16916  nnnninfex  16926  trilpolemclim  16946  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  trirec0  16954  apdifflemf  16956  apdifflemr  16957  apdiff  16958  iswomni0  16962  trimul0or  16971  nconstwlpolemgt0  16976  nconstwlpolem  16977  neapmkvlem  16979