Theorem mpjaodan 810

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjao3dan  1348  dcun  3637  ifcldadc  3670  ifeq1dadc  3671  ifeq2dadc  3672  ifeqdadc  3673  ifbothdadc  3674  ifcldcd  3678  2if2dc  3680  ifeqeqxdc  3687  exmidn0m  4338  exmidsssn  4339  exmidundif  4343  exmidundifim  4344  ordtri2or2exmidlem  4673  reg2exmidlema  4681  nnpredcl  4770  frecabcl  6670  nnsucuniel  6768  dcdifsnid  6777  pw2f1odclem  7134  phpm  7167  fidifsnen  7172  dif1enen  7184  fin0  7189  fimax2gtrilemstep  7205  finexdc  7207  elssdc  7209  eqsndc  7210  en2eqpr  7214  fientri3  7222  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  prfidceq  7235  tpfidceq  7237  fiintim  7238  ssfirab  7244  fidcenumlemrks  7270  fidcenumlemr  7272  2omap  7318  omp1eomlem  7434  difinfsnlem  7439  difinfsn  7440  ctssdccl  7451  ctssdc  7453  enumct  7455  nninfninc  7463  nnnninf  7466  nnnninfeq  7468  nnnninfeq2  7469  nninfisol  7473  finomni  7480  ismkvnex  7495  nninfwlpoimlemg  7515  pr2cv1  7541  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  exmidontriimlem3  7579  netap  7620  2omotaplemap  7623  mullocprlem  7937  recexprlemloc  7998  suplocsrlem  8175  btwnapz  9776  xnn0dcle  10204  xnn0letri  10205  z2ge  10228  xaddcom  10263  xnegdi  10270  xaddass  10271  xpncan  10273  xleadd1a  10275  xsubge0  10283  xlesubadd  10285  fztri3or  10443  fzm1  10507  fzneuz  10508  exfzdc  10659  zsupcllemstep  10662  infssuzex  10666  exbtwnzlemstep  10682  rebtwn2zlemstep  10687  xqltnle  10702  apbtwnz  10709  modifeq2int  10823  modsumfzodifsn  10833  iseqf1olemab  10939  iseqf1olemmo  10942  seq3f1olemqsumk  10949  seq3f1olemqsum  10950  seq3f1olemstep  10951  seqf1oglem1  10956  seqf1oglem2  10957  fser0const  10972  expaddzaplem  11019  qsqeqor  11087  resq01  11095  expnbnd  11101  nn0ltexp2  11147  apexp1  11156  bcval  11187  bccmpl  11192  bcval5  11201  bcpasc  11204  bccl  11205  hashennnuni  11218  hashnncl  11234  fiubm  11271  hashfibc  11283  hashf1  11287  zfz1isolemiso  11291  lswex  11356  ccatsymb  11370  ccat1st1st  11409  fzowrddc  11419  swrd0g  11432  swrdsbslen  11438  swrdspsleq  11439  pfxclz  11451  pfxwrdsymbg  11462  swrdccatin1  11497  resqrexlemnm  11784  resqrexlemcvg  11785  resqrexlemoverl  11787  resqrexlemglsq  11788  leabs  11840  nn0abscl  11851  ltabs  11853  abslt  11854  fzomaxdif  11879  maxleim  11971  maxabslemval  11974  zmaxcl  11990  2zsupmax  11992  minmax  11996  2zinfmin  12009  xrmaxleim  12010  xrmaxifle  12012  xrmaxiflemab  12013  xrmaxiflemlub  12014  xrmaxiflemcom  12015  xrmaxiflemval  12016  xrmaxaddlem  12026  xrmaxadd  12027  xrminmax  12031  sumdc  12124  fzf1o  12142  sumrbdc  12146  summodclem3  12147  summodclem2a  12148  zsumdc  12151  isumss  12158  fisumss  12159  isumss2  12160  fsumcllem  12166  fsumadd  12173  fsumsplit  12174  fsumsplitsn  12177  sumsplitdc  12199  fisumrev2  12213  fsummulc2  12215  telfsumo  12233  fsumparts  12237  cvgratnnlemseq  12293  cvgratz  12299  fproddccvg  12339  prodrbdc  12341  zproddc  12346  prod1dc  12353  fprodssdc  12357  fprodmul  12358  fprodsplitdc  12363  fprodsplit  12364  fprodunsn  12371  fprodcllem  12373  sinltxirr  12528  fsumdvds  12609  dvdsle  12611  mod2eq1n2dvds  12646  bitsmod  12723  gcdsupex  12734  gcdsupcl  12735  gcdval  12736  gcddvds  12740  gcdcl  12743  gcd0id  12756  gcdneg  12759  bezoutlemmain  12775  bezoutlemzz  12779  bezoutlemaz  12780  bezoutlembz  12781  dfgcd3  12787  dfgcd2  12791  nninfctlemfo  12817  nn0seqcvgd  12819  eucalgf  12833  eucalginv  12834  dvdslcm  12847  lcmcl  12850  lcmneg  12852  lcmgcd  12856  lcmdvds  12857  lcmid  12858  mulgcddvds  12872  isprm5lem  12919  pw2dvdslemn  12943  sqrt2irrap  12958  phibndlem  12994  prm23ge5  13043  pclemdc  13067  pcxqcl  13091  pcge0  13092  pcdvdsb  13099  pceq0  13101  pcneg  13104  pcdvdstr  13106  pcgcd1  13107  pcgcd  13108  pc2dvds  13109  pcz  13111  pcprmpw2  13112  pcaddlem  13118  pcadd  13119  pcmpt  13122  pcmpt2  13123  pcprod  13125  fldivp1  13127  qexpz  13131  1arithlem4  13145  1arith  13146  4sqlem19  13188  ennnfonelemss  13301  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ctiunctlemudc  13328  bassetsnn  13409  fvprif  13664  gzsumwsubmcl  13801  gzsumwmhm  13803  gzsumcl  13804  mulgnn0p1  13936  mulgnn0subcl  13938  mulgsubcl  13939  mulgneg  13943  mulgz  13953  mulgnn0dir  13955  mulgdirlem  13956  mulgdir  13957  submmulg  13969  ghmmulg  14059  gzsumreidx  14141  gzsumsubmcl  14142  gzsummhm  14145  gzsumsplit0  14148  gsumvalfi  14152  gzsumgsum  14155  lringuplu  14503  aprlring  14600  znf1o  14986  xblss2ps  15505  xblss2  15506  qtopbas  15623  dedekindeulemeu  15723  dedekindeu  15724  suplociccreex  15725  dedekindicclemeu  15732  dedekindicclemicc  15733  limcimolemlt  15765  cnplimclemle  15769  dvmptc  15818  reeff1o  15874  efltlemlt  15875  sin0pilem2  15883  coseq0negpitopi  15937  abssinper  15947  cos02pilt1  15952  logbgcd1irraplemexp  16070  birthdaylem2  16088  birthdaylem3  16089  lgslem4  16122  lgsneg  16143  lgsneg1  16144  lgsmod  16145  lgsdilem  16146  lgsdir2  16152  lgsdirprm  16153  lgsdir  16154  lgsdi  16156  lgsne0  16157  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  gausslemma2dlem4  16183  lgseisenlem1  16189  lgsquad3  16203  2sqlem4  16237  2sqlem9  16243  eupth2lem3lem3fi  16711  eupth2lem3lem4fi  16714  eupth2lem3lem7fi  16715  dichmul0orlem3  16755  dichmul0orlem7  16759  nnsf  17048  nninfsellemsuc  17055  nnnninfex  17065  trilpolemclim  17085  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  trirec0  17093  apdifflemf  17095  apdifflemr  17096  apdiff  17097  iswomni0  17101  nconstwlpolemgt0  17114  nconstwlpolem  17115  neapmkvlem  17117