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

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  3570  ifcldadc  3600  ifeq1dadc  3601  ifeq2dadc  3602  ifeqdadc  3603  ifbothdadc  3604  ifcldcd  3608  exmidn0m  4245  exmidsssn  4246  exmidundif  4250  exmidundifim  4251  ordtri2or2exmidlem  4574  reg2exmidlema  4582  nnpredcl  4671  frecabcl  6485  nnsucuniel  6581  dcdifsnid  6590  pw2f1odclem  6931  phpm  6962  fidifsnen  6967  dif1enen  6977  fin0  6982  fimax2gtrilemstep  6997  finexdc  6999  en2eqpr  7004  fientri3  7012  unsnfidcex  7017  unsnfidcel  7018  undifdcss  7020  prfidceq  7025  tpfidceq  7027  fiintim  7028  ssfirab  7033  fidcenumlemrks  7055  fidcenumlemr  7057  omp1eomlem  7196  difinfsnlem  7201  difinfsn  7202  ctssdccl  7213  ctssdc  7215  enumct  7217  nninfninc  7225  nnnninf  7228  nnnninfeq  7230  nnnninfeq2  7231  nninfisol  7235  finomni  7242  ismkvnex  7257  nninfwlpoimlemg  7277  exmidfodomrlemeldju  7307  exmidfodomrlemreseldju  7308  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidaclem  7320  exmidontriimlem3  7335  netap  7366  2omotaplemap  7369  mullocprlem  7683  recexprlemloc  7744  suplocsrlem  7921  btwnapz  9503  xnn0dcle  9924  xnn0letri  9925  z2ge  9948  xaddcom  9983  xnegdi  9990  xaddass  9991  xpncan  9993  xleadd1a  9995  xsubge0  10003  xlesubadd  10005  fztri3or  10161  fzm1  10222  fzneuz  10223  exfzdc  10369  zsupcllemstep  10372  infssuzex  10376  exbtwnzlemstep  10390  rebtwn2zlemstep  10395  xqltnle  10410  apbtwnz  10417  modifeq2int  10531  modsumfzodifsn  10541  iseqf1olemab  10647  iseqf1olemmo  10650  seq3f1olemqsumk  10657  seq3f1olemqsum  10658  seq3f1olemstep  10659  seqf1oglem1  10664  seqf1oglem2  10665  fser0const  10680  expaddzaplem  10727  qsqeqor  10795  expnbnd  10808  nn0ltexp2  10854  apexp1  10863  bcval  10894  bccmpl  10899  bcval5  10908  bcpasc  10911  bccl  10912  hashennnuni  10924  hashnncl  10940  fiubm  10973  zfz1isolemiso  10984  ccatsymb  11058  ccat1st1st  11093  fzowrddc  11100  swrd0g  11113  swrdsbslen  11119  swrdspsleq  11120  resqrexlemnm  11329  resqrexlemcvg  11330  resqrexlemoverl  11332  resqrexlemglsq  11333  leabs  11385  nn0abscl  11396  ltabs  11398  abslt  11399  fzomaxdif  11424  maxleim  11516  maxabslemval  11519  zmaxcl  11535  2zsupmax  11537  minmax  11541  2zinfmin  11554  xrmaxleim  11555  xrmaxifle  11557  xrmaxiflemab  11558  xrmaxiflemlub  11559  xrmaxiflemcom  11560  xrmaxiflemval  11561  xrmaxaddlem  11571  xrmaxadd  11572  xrminmax  11576  sumdc  11669  sumrbdc  11690  summodclem3  11691  summodclem2a  11692  zsumdc  11695  isumss  11702  fisumss  11703  isumss2  11704  fsumcllem  11710  fsumadd  11717  fsumsplit  11718  fsumsplitsn  11721  sumsplitdc  11743  fisumrev2  11757  fsummulc2  11759  telfsumo  11777  fsumparts  11781  cvgratnnlemseq  11837  cvgratz  11843  fproddccvg  11883  prodrbdc  11885  zproddc  11890  prod1dc  11897  fprodssdc  11901  fprodmul  11902  fprodsplitdc  11907  fprodsplit  11908  fprodunsn  11915  fprodcllem  11917  sinltxirr  12072  fsumdvds  12153  dvdsle  12155  mod2eq1n2dvds  12190  bitsmod  12267  gcdsupex  12278  gcdsupcl  12279  gcdval  12280  gcddvds  12284  gcdcl  12287  gcd0id  12300  gcdneg  12303  bezoutlemmain  12319  bezoutlemzz  12323  bezoutlemaz  12324  bezoutlembz  12325  dfgcd3  12331  dfgcd2  12335  nninfctlemfo  12361  nn0seqcvgd  12363  eucalgf  12377  eucalginv  12378  dvdslcm  12391  lcmcl  12394  lcmneg  12396  lcmgcd  12400  lcmdvds  12401  lcmid  12402  mulgcddvds  12416  isprm5lem  12463  pw2dvdslemn  12487  sqrt2irrap  12502  phibndlem  12538  prm23ge5  12587  pclemdc  12611  pcxqcl  12635  pcge0  12636  pcdvdsb  12643  pceq0  12645  pcneg  12648  pcdvdstr  12650  pcgcd1  12651  pcgcd  12652  pc2dvds  12653  pcz  12655  pcprmpw2  12656  pcaddlem  12662  pcadd  12663  pcmpt  12666  pcmpt2  12667  pcprod  12669  fldivp1  12671  qexpz  12675  1arithlem4  12689  1arith  12690  4sqlem19  12732  ennnfonelemss  12781  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ctiunctlemudc  12808  fvprif  13175  gsumfzz  13327  gsumwsubmcl  13328  gsumwmhm  13330  gsumfzcl  13331  mulgnn0p1  13469  mulgnn0subcl  13471  mulgsubcl  13472  mulgneg  13476  mulgz  13486  mulgnn0dir  13488  mulgdirlem  13489  mulgdir  13490  submmulg  13502  ghmmulg  13592  gsumfzreidx  13673  gsumfzsubmcl  13674  gsumfzmptfidmadd  13675  gsumfzmhm  13679  lringuplu  13958  gsumfzfsum  14350  znf1o  14413  xblss2ps  14876  xblss2  14877  qtopbas  14994  dedekindeulemeu  15094  dedekindeu  15095  suplociccreex  15096  dedekindicclemeu  15103  dedekindicclemicc  15104  limcimolemlt  15136  cnplimclemle  15140  dvmptc  15189  reeff1o  15245  efltlemlt  15246  sin0pilem2  15254  coseq0negpitopi  15308  abssinper  15318  cos02pilt1  15323  logbgcd1irraplemexp  15440  lgslem4  15480  lgsneg  15501  lgsneg1  15502  lgsmod  15503  lgsdilem  15504  lgsdir2  15510  lgsdirprm  15511  lgsdir  15512  lgsdi  15514  lgsne0  15515  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  gausslemma2dlem4  15541  lgseisenlem1  15547  lgsquad3  15561  2sqlem4  15595  2sqlem9  15601  2omap  15932  nnsf  15942  nninfsellemsuc  15949  nnnninfex  15959  trilpolemclim  15975  trilpolemisumle  15977  trilpolemeq1  15979  trilpolemlt1  15980  trirec0  15983  apdifflemf  15985  apdifflemr  15986  apdiff  15987  iswomni0  15990  nconstwlpolemgt0  16003  nconstwlpolem  16004  neapmkvlem  16006