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  3601  ifcldadc  3632  ifeq1dadc  3633  ifeq2dadc  3634  ifeqdadc  3635  ifbothdadc  3636  ifcldcd  3640  2if2dc  3642  exmidn0m  4285  exmidsssn  4286  exmidundif  4290  exmidundifim  4291  ordtri2or2exmidlem  4618  reg2exmidlema  4626  nnpredcl  4715  frecabcl  6551  nnsucuniel  6649  dcdifsnid  6658  pw2f1odclem  7003  phpm  7035  fidifsnen  7040  dif1enen  7050  fin0  7055  fimax2gtrilemstep  7071  finexdc  7073  elssdc  7075  eqsndc  7076  en2eqpr  7080  fientri3  7088  unsnfidcex  7093  unsnfidcel  7094  undifdcss  7096  prfidceq  7101  tpfidceq  7103  fiintim  7104  ssfirab  7109  fidcenumlemrks  7131  fidcenumlemr  7133  omp1eomlem  7272  difinfsnlem  7277  difinfsn  7278  ctssdccl  7289  ctssdc  7291  enumct  7293  nninfninc  7301  nnnninf  7304  nnnninfeq  7306  nnnninfeq2  7307  nninfisol  7311  finomni  7318  ismkvnex  7333  nninfwlpoimlemg  7353  pr2cv1  7379  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidaclem  7401  exmidontriimlem3  7416  netap  7451  2omotaplemap  7454  mullocprlem  7768  recexprlemloc  7829  suplocsrlem  8006  btwnapz  9588  xnn0dcle  10010  xnn0letri  10011  z2ge  10034  xaddcom  10069  xnegdi  10076  xaddass  10077  xpncan  10079  xleadd1a  10081  xsubge0  10089  xlesubadd  10091  fztri3or  10247  fzm1  10308  fzneuz  10309  exfzdc  10458  zsupcllemstep  10461  infssuzex  10465  exbtwnzlemstep  10479  rebtwn2zlemstep  10484  xqltnle  10499  apbtwnz  10506  modifeq2int  10620  modsumfzodifsn  10630  iseqf1olemab  10736  iseqf1olemmo  10739  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1olemstep  10748  seqf1oglem1  10753  seqf1oglem2  10754  fser0const  10769  expaddzaplem  10816  qsqeqor  10884  expnbnd  10897  nn0ltexp2  10943  apexp1  10952  bcval  10983  bccmpl  10988  bcval5  10997  bcpasc  11000  bccl  11001  hashennnuni  11013  hashnncl  11029  fiubm  11063  zfz1isolemiso  11074  lswex  11136  ccatsymb  11150  ccat1st1st  11188  fzowrddc  11195  swrd0g  11208  swrdsbslen  11214  swrdspsleq  11215  pfxclz  11227  pfxwrdsymbg  11238  swrdccatin1  11273  resqrexlemnm  11545  resqrexlemcvg  11546  resqrexlemoverl  11548  resqrexlemglsq  11549  leabs  11601  nn0abscl  11612  ltabs  11614  abslt  11615  fzomaxdif  11640  maxleim  11732  maxabslemval  11735  zmaxcl  11751  2zsupmax  11753  minmax  11757  2zinfmin  11770  xrmaxleim  11771  xrmaxifle  11773  xrmaxiflemab  11774  xrmaxiflemlub  11775  xrmaxiflemcom  11776  xrmaxiflemval  11777  xrmaxaddlem  11787  xrmaxadd  11788  xrminmax  11792  sumdc  11885  sumrbdc  11906  summodclem3  11907  summodclem2a  11908  zsumdc  11911  isumss  11918  fisumss  11919  isumss2  11920  fsumcllem  11926  fsumadd  11933  fsumsplit  11934  fsumsplitsn  11937  sumsplitdc  11959  fisumrev2  11973  fsummulc2  11975  telfsumo  11993  fsumparts  11997  cvgratnnlemseq  12053  cvgratz  12059  fproddccvg  12099  prodrbdc  12101  zproddc  12106  prod1dc  12113  fprodssdc  12117  fprodmul  12118  fprodsplitdc  12123  fprodsplit  12124  fprodunsn  12131  fprodcllem  12133  sinltxirr  12288  fsumdvds  12369  dvdsle  12371  mod2eq1n2dvds  12406  bitsmod  12483  gcdsupex  12494  gcdsupcl  12495  gcdval  12496  gcddvds  12500  gcdcl  12503  gcd0id  12516  gcdneg  12519  bezoutlemmain  12535  bezoutlemzz  12539  bezoutlemaz  12540  bezoutlembz  12541  dfgcd3  12547  dfgcd2  12551  nninfctlemfo  12577  nn0seqcvgd  12579  eucalgf  12593  eucalginv  12594  dvdslcm  12607  lcmcl  12610  lcmneg  12612  lcmgcd  12616  lcmdvds  12617  lcmid  12618  mulgcddvds  12632  isprm5lem  12679  pw2dvdslemn  12703  sqrt2irrap  12718  phibndlem  12754  prm23ge5  12803  pclemdc  12827  pcxqcl  12851  pcge0  12852  pcdvdsb  12859  pceq0  12861  pcneg  12864  pcdvdstr  12866  pcgcd1  12867  pcgcd  12868  pc2dvds  12869  pcz  12871  pcprmpw2  12872  pcaddlem  12878  pcadd  12879  pcmpt  12882  pcmpt2  12883  pcprod  12885  fldivp1  12887  qexpz  12891  1arithlem4  12905  1arith  12906  4sqlem19  12948  ennnfonelemss  12997  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ctiunctlemudc  13024  bassetsnn  13105  fvprif  13392  gsumfzz  13544  gsumwsubmcl  13545  gsumwmhm  13547  gsumfzcl  13548  mulgnn0p1  13686  mulgnn0subcl  13688  mulgsubcl  13689  mulgneg  13693  mulgz  13703  mulgnn0dir  13705  mulgdirlem  13706  mulgdir  13707  submmulg  13719  ghmmulg  13809  gsumfzreidx  13890  gsumfzsubmcl  13891  gsumfzmptfidmadd  13892  gsumfzmhm  13896  lringuplu  14176  gsumfzfsum  14568  znf1o  14631  xblss2ps  15094  xblss2  15095  qtopbas  15212  dedekindeulemeu  15312  dedekindeu  15313  suplociccreex  15314  dedekindicclemeu  15321  dedekindicclemicc  15322  limcimolemlt  15354  cnplimclemle  15358  dvmptc  15407  reeff1o  15463  efltlemlt  15464  sin0pilem2  15472  coseq0negpitopi  15526  abssinper  15536  cos02pilt1  15541  logbgcd1irraplemexp  15658  lgslem4  15698  lgsneg  15719  lgsneg1  15720  lgsmod  15721  lgsdilem  15722  lgsdir2  15728  lgsdirprm  15729  lgsdir  15730  lgsdi  15732  lgsne0  15733  lgsdirnn0  15742  lgsdinn0  15743  gausslemma2dlem1a  15753  gausslemma2dlem1f1o  15755  gausslemma2dlem4  15759  lgseisenlem1  15765  lgsquad3  15779  2sqlem4  15813  2sqlem9  15819  2omap  16446  nnsf  16459  nninfsellemsuc  16466  nnnninfex  16476  trilpolemclim  16492  trilpolemisumle  16494  trilpolemeq1  16496  trilpolemlt1  16497  trirec0  16500  apdifflemf  16502  apdifflemr  16503  apdiff  16504  iswomni0  16507  nconstwlpolemgt0  16520  nconstwlpolem  16521  neapmkvlem  16523