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  3602  ifcldadc  3633  ifeq1dadc  3634  ifeq2dadc  3635  ifeqdadc  3636  ifbothdadc  3637  ifcldcd  3641  2if2dc  3643  exmidn0m  4289  exmidsssn  4290  exmidundif  4294  exmidundifim  4295  ordtri2or2exmidlem  4622  reg2exmidlema  4630  nnpredcl  4719  frecabcl  6560  nnsucuniel  6658  dcdifsnid  6667  pw2f1odclem  7015  phpm  7047  fidifsnen  7052  dif1enen  7062  fin0  7067  fimax2gtrilemstep  7083  finexdc  7085  elssdc  7087  eqsndc  7088  en2eqpr  7092  fientri3  7100  unsnfidcex  7105  unsnfidcel  7106  undifdcss  7108  prfidceq  7113  tpfidceq  7115  fiintim  7116  ssfirab  7121  fidcenumlemrks  7143  fidcenumlemr  7145  omp1eomlem  7284  difinfsnlem  7289  difinfsn  7290  ctssdccl  7301  ctssdc  7303  enumct  7305  nninfninc  7313  nnnninf  7316  nnnninfeq  7318  nnnninfeq2  7319  nninfisol  7323  finomni  7330  ismkvnex  7345  nninfwlpoimlemg  7365  pr2cv1  7391  exmidfodomrlemeldju  7400  exmidfodomrlemreseldju  7401  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidaclem  7413  exmidontriimlem3  7428  netap  7463  2omotaplemap  7466  mullocprlem  7780  recexprlemloc  7841  suplocsrlem  8018  btwnapz  9600  xnn0dcle  10027  xnn0letri  10028  z2ge  10051  xaddcom  10086  xnegdi  10093  xaddass  10094  xpncan  10096  xleadd1a  10098  xsubge0  10106  xlesubadd  10108  fztri3or  10264  fzm1  10325  fzneuz  10326  exfzdc  10476  zsupcllemstep  10479  infssuzex  10483  exbtwnzlemstep  10497  rebtwn2zlemstep  10502  xqltnle  10517  apbtwnz  10524  modifeq2int  10638  modsumfzodifsn  10648  iseqf1olemab  10754  iseqf1olemmo  10757  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  seq3f1olemstep  10766  seqf1oglem1  10771  seqf1oglem2  10772  fser0const  10787  expaddzaplem  10834  qsqeqor  10902  expnbnd  10915  nn0ltexp2  10961  apexp1  10970  bcval  11001  bccmpl  11006  bcval5  11015  bcpasc  11018  bccl  11019  hashennnuni  11031  hashnncl  11047  fiubm  11082  zfz1isolemiso  11093  lswex  11155  ccatsymb  11169  ccat1st1st  11208  fzowrddc  11218  swrd0g  11231  swrdsbslen  11237  swrdspsleq  11238  pfxclz  11250  pfxwrdsymbg  11261  swrdccatin1  11296  resqrexlemnm  11569  resqrexlemcvg  11570  resqrexlemoverl  11572  resqrexlemglsq  11573  leabs  11625  nn0abscl  11636  ltabs  11638  abslt  11639  fzomaxdif  11664  maxleim  11756  maxabslemval  11759  zmaxcl  11775  2zsupmax  11777  minmax  11781  2zinfmin  11794  xrmaxleim  11795  xrmaxifle  11797  xrmaxiflemab  11798  xrmaxiflemlub  11799  xrmaxiflemcom  11800  xrmaxiflemval  11801  xrmaxaddlem  11811  xrmaxadd  11812  xrminmax  11816  sumdc  11909  sumrbdc  11930  summodclem3  11931  summodclem2a  11932  zsumdc  11935  isumss  11942  fisumss  11943  isumss2  11944  fsumcllem  11950  fsumadd  11957  fsumsplit  11958  fsumsplitsn  11961  sumsplitdc  11983  fisumrev2  11997  fsummulc2  11999  telfsumo  12017  fsumparts  12021  cvgratnnlemseq  12077  cvgratz  12083  fproddccvg  12123  prodrbdc  12125  zproddc  12130  prod1dc  12137  fprodssdc  12141  fprodmul  12142  fprodsplitdc  12147  fprodsplit  12148  fprodunsn  12155  fprodcllem  12157  sinltxirr  12312  fsumdvds  12393  dvdsle  12395  mod2eq1n2dvds  12430  bitsmod  12507  gcdsupex  12518  gcdsupcl  12519  gcdval  12520  gcddvds  12524  gcdcl  12527  gcd0id  12540  gcdneg  12543  bezoutlemmain  12559  bezoutlemzz  12563  bezoutlemaz  12564  bezoutlembz  12565  dfgcd3  12571  dfgcd2  12575  nninfctlemfo  12601  nn0seqcvgd  12603  eucalgf  12617  eucalginv  12618  dvdslcm  12631  lcmcl  12634  lcmneg  12636  lcmgcd  12640  lcmdvds  12641  lcmid  12642  mulgcddvds  12656  isprm5lem  12703  pw2dvdslemn  12727  sqrt2irrap  12742  phibndlem  12778  prm23ge5  12827  pclemdc  12851  pcxqcl  12875  pcge0  12876  pcdvdsb  12883  pceq0  12885  pcneg  12888  pcdvdstr  12890  pcgcd1  12891  pcgcd  12892  pc2dvds  12893  pcz  12895  pcprmpw2  12896  pcaddlem  12902  pcadd  12903  pcmpt  12906  pcmpt2  12907  pcprod  12909  fldivp1  12911  qexpz  12915  1arithlem4  12929  1arith  12930  4sqlem19  12972  ennnfonelemss  13021  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ctiunctlemudc  13048  bassetsnn  13129  fvprif  13416  gsumfzz  13568  gsumwsubmcl  13569  gsumwmhm  13571  gsumfzcl  13572  mulgnn0p1  13710  mulgnn0subcl  13712  mulgsubcl  13713  mulgneg  13717  mulgz  13727  mulgnn0dir  13729  mulgdirlem  13730  mulgdir  13731  submmulg  13743  ghmmulg  13833  gsumfzreidx  13914  gsumfzsubmcl  13915  gsumfzmptfidmadd  13916  gsumfzmhm  13920  lringuplu  14200  gsumfzfsum  14592  znf1o  14655  xblss2ps  15118  xblss2  15119  qtopbas  15236  dedekindeulemeu  15336  dedekindeu  15337  suplociccreex  15338  dedekindicclemeu  15345  dedekindicclemicc  15346  limcimolemlt  15378  cnplimclemle  15382  dvmptc  15431  reeff1o  15487  efltlemlt  15488  sin0pilem2  15496  coseq0negpitopi  15550  abssinper  15560  cos02pilt1  15565  logbgcd1irraplemexp  15682  lgslem4  15722  lgsneg  15743  lgsneg1  15744  lgsmod  15745  lgsdilem  15746  lgsdir2  15752  lgsdirprm  15753  lgsdir  15754  lgsdi  15756  lgsne0  15757  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem4  15783  lgseisenlem1  15789  lgsquad3  15803  2sqlem4  15837  2sqlem9  15843  2omap  16530  nnsf  16543  nninfsellemsuc  16550  nnnninfex  16560  trilpolemclim  16576  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  trirec0  16584  apdifflemf  16586  apdifflemr  16587  apdiff  16588  iswomni0  16591  nconstwlpolemgt0  16604  nconstwlpolem  16605  neapmkvlem  16607