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  sn0disj  4127  exmidn0m  4340  exmidsssn  4341  exmidundif  4345  exmidundifim  4346  ordtri2or2exmidlem  4675  reg2exmidlema  4683  nnpredcl  4772  frecabcl  6675  nnsucuniel  6773  dcdifsnid  6782  pw2f1odclem  7140  phpm  7173  fidifsnen  7178  dif1enen  7190  fin0  7195  fimax2gtrilemstep  7211  finexdc  7213  elssdc  7215  eqsndc  7216  en2eqpr  7220  fientri3  7228  unsnfidcex  7233  unsnfidcel  7234  undifdcss  7236  prfidceq  7241  tpfidceq  7243  fiintim  7244  ssfirab  7250  fidcenumlemrks  7277  fidcenumlemr  7279  2omap  7324  omp1eomlem  7440  difinfsnlem  7445  difinfsn  7446  ctssdccl  7457  ctssdc  7459  enumct  7461  nninfninc  7469  nnnninf  7472  nnnninfeq  7474  nnnninfeq2  7475  nninfisol  7479  finomni  7486  ismkvnex  7501  nninfwlpoimlemg  7521  pr2cv1  7547  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  exmidontriimlem3  7585  netap  7626  2omotaplemap  7629  mullocprlem  7943  recexprlemloc  8004  suplocsrlem  8181  btwnapz  9786  xnn0dcle  10220  xnn0letri  10221  z2ge  10244  xaddcom  10279  xnegdi  10286  xaddass  10287  xpncan  10289  xleadd1a  10291  xsubge0  10299  xlesubadd  10301  fztri3or  10459  fzm1  10523  fzneuz  10524  exfzdc  10675  zsupcllemstep  10678  infssuzex  10682  exbtwnzlemstep  10698  rebtwn2zlemstep  10703  xqltnle  10718  apbtwnz  10725  flaplt  10738  modifeq2int  10843  modsumfzodifsn  10853  iseqf1olemab  10959  iseqf1olemmo  10962  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  seq3f1olemstep  10971  seqf1oglem1  10976  seqf1oglem2  10977  fser0const  10992  expaddzaplem  11039  qsqeqor  11107  resq01  11115  expnbnd  11121  nn0ltexp2  11168  apexp1  11177  bcval  11208  bccmpl  11213  bcval5  11222  bcpasc  11225  bccl  11226  hashennnuni  11239  hashnncl  11255  fiubm  11292  hashfibc  11304  hashf1  11308  zfz1isolemiso  11312  lswex  11377  ccatsymb  11391  ccat1st1st  11430  fzowrddc  11440  swrd0g  11453  swrdsbslen  11459  swrdspsleq  11460  pfxclz  11472  pfxwrdsymbg  11483  swrdccatin1  11518  resqrexlemnm  11805  resqrexlemcvg  11806  resqrexlemoverl  11808  resqrexlemglsq  11809  leabs  11861  qabscl  11864  nn0abscl  11873  ltabs  11875  abslt  11876  fzomaxdif  11901  maxleim  11993  maxabslemval  11996  zmaxcl  12012  2zsupmax  12014  minmax  12019  zmincl  12028  2zinfmin  12033  xrmaxleim  12034  xrmaxifle  12036  xrmaxiflemab  12037  xrmaxiflemlub  12038  xrmaxiflemcom  12039  xrmaxiflemval  12040  xrmaxaddlem  12050  xrmaxadd  12051  xrminmax  12055  sumdc  12148  fzf1o  12166  sumrbdc  12170  summodclem3  12171  summodclem2a  12172  zsumdc  12175  isumss  12182  fisumss  12183  isumss2  12184  fsumcllem  12190  fsumadd  12197  fsumsplit  12198  fsumsplitsn  12201  sumsplitdc  12223  fisumrev2  12237  fsummulc2  12239  telfsumo  12257  fsumparts  12261  cvgratnnlemseq  12317  cvgratz  12323  fproddccvg  12363  prodrbdc  12365  zproddc  12370  prod1dc  12377  fprodssdc  12381  fprodmul  12382  fprodsplitdc  12387  fprodsplit  12388  fprodunsn  12395  fprodcllem  12397  sinltxirr  12552  fsumdvds  12633  dvdsle  12635  mod2eq1n2dvds  12670  bitsmod  12747  gcdsupex  12758  gcdsupcl  12759  gcdval  12760  gcddvds  12764  gcdcl  12767  gcd0id  12780  gcdneg  12783  bezoutlemmain  12799  bezoutlemzz  12803  bezoutlemaz  12804  bezoutlembz  12805  dfgcd3  12811  dfgcd2  12815  nninfctlemfo  12841  nn0seqcvgd  12843  eucalgf  12857  eucalginv  12858  dvdslcm  12871  lcmcl  12874  lcmneg  12876  lcmgcd  12880  lcmdvds  12881  lcmid  12882  mulgcddvds  12896  prmdcz  12933  isprm5lem  12944  pwbdvdslemn  12968  sqrt2irrap  12984  sqrtrirr  13013  phibndlem  13022  prm23ge5  13071  pclemdc  13095  pcxqcl  13119  pcge0  13120  pcdvdsb  13127  pceq0  13129  pcneg  13132  pcdvdstr  13134  pcgcd1  13135  pcgcd  13136  pc2dvds  13137  pcz  13139  pcprmpw2  13140  pcaddlem  13146  pcadd  13147  pcmpt  13150  pcmpt2  13151  pcprod  13153  fldivp1  13155  qexpz  13159  1arithlem4  13173  1arith  13174  4sqlem19  13216  ennnfonelemss  13358  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ctiunctlemudc  13385  bassetsnn  13466  fvprif  13722  gzsumwsubmcl  13859  gzsumwmhm  13861  gzsumcl  13862  mulgnn0p1  13994  mulgnn0subcl  13996  mulgsubcl  13997  mulgneg  14001  mulgz  14011  mulgnn0dir  14013  mulgdirlem  14014  mulgdir  14015  submmulg  14027  ghmmulg  14117  gzsumreidx  14230  gzsumsubmcl  14231  gzsummhm  14234  gzsumsplit0  14237  gsumvalfi  14241  gzsumgsum  14244  gsummptfidmsplit  14253  gsumresfi  14262  gsum2d2fi  14273  lringuplu  14611  aprlring  14708  znf1o  15094  xblss2ps  15647  xblss2  15648  qtopbas  15765  dedekindeulemeu  15865  dedekindeu  15866  suplociccreex  15867  dedekindicclemeu  15874  dedekindicclemicc  15875  limcimolemlt  15907  cnplimclemle  15911  dvmptc  15960  reeff1o  16016  efltlemlt  16017  efap1p  16022  sin0pilem2  16026  coseq0negpitopi  16080  abssinper  16090  cos02pilt1  16096  logdivlt  16141  logbgcd1irraplemexp  16221  birthdaylem2  16243  birthdaylem3  16244  ppiqp1le  16284  ppiqltx  16298  ppiqub  16310  chtqub  16313  bcmono  16321  bcmax  16322  bposlem3  16330  bposlem5  16332  bposlem6  16333  bpos  16337  lgslem4  16344  lgsneg  16365  lgsneg1  16366  lgsmod  16367  lgsdilem  16368  lgsdir2  16374  lgsdirprm  16375  lgsdir  16376  lgsdi  16378  lgsne0  16379  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  gausslemma2dlem4  16405  lgseisenlem1  16411  lgsquad3  16425  2sqlem4  16459  2sqlem9  16465  eupth2lem3lem3fi  16933  eupth2lem3lem4fi  16936  eupth2lem3lem7fi  16937  dichmul0orlem3  16977  dichmul0orlem7  16981  nnsf  17271  nninfsellemsuc  17278  nnnninfex  17288  trilpolemclim  17309  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  trirec0  17317  apdifflemf  17319  apdifflemr  17320  apdiff  17321  iswomni0  17325  nconstwlpolemgt0  17338  nconstwlpolem  17339  neapmkvlem  17341