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  3578  ifcldadc  3609  ifeq1dadc  3610  ifeq2dadc  3611  ifeqdadc  3612  ifbothdadc  3613  ifcldcd  3617  2if2dc  3619  exmidn0m  4261  exmidsssn  4262  exmidundif  4266  exmidundifim  4267  ordtri2or2exmidlem  4592  reg2exmidlema  4600  nnpredcl  4689  frecabcl  6508  nnsucuniel  6604  dcdifsnid  6613  pw2f1odclem  6956  phpm  6988  fidifsnen  6993  dif1enen  7003  fin0  7008  fimax2gtrilemstep  7023  finexdc  7025  en2eqpr  7030  fientri3  7038  unsnfidcex  7043  unsnfidcel  7044  undifdcss  7046  prfidceq  7051  tpfidceq  7053  fiintim  7054  ssfirab  7059  fidcenumlemrks  7081  fidcenumlemr  7083  omp1eomlem  7222  difinfsnlem  7227  difinfsn  7228  ctssdccl  7239  ctssdc  7241  enumct  7243  nninfninc  7251  nnnninf  7254  nnnninfeq  7256  nnnninfeq2  7257  nninfisol  7261  finomni  7268  ismkvnex  7283  nninfwlpoimlemg  7303  pr2cv1  7329  exmidfodomrlemeldju  7338  exmidfodomrlemreseldju  7339  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidaclem  7351  exmidontriimlem3  7366  netap  7401  2omotaplemap  7404  mullocprlem  7718  recexprlemloc  7779  suplocsrlem  7956  btwnapz  9538  xnn0dcle  9959  xnn0letri  9960  z2ge  9983  xaddcom  10018  xnegdi  10025  xaddass  10026  xpncan  10028  xleadd1a  10030  xsubge0  10038  xlesubadd  10040  fztri3or  10196  fzm1  10257  fzneuz  10258  exfzdc  10406  zsupcllemstep  10409  infssuzex  10413  exbtwnzlemstep  10427  rebtwn2zlemstep  10432  xqltnle  10447  apbtwnz  10454  modifeq2int  10568  modsumfzodifsn  10578  iseqf1olemab  10684  iseqf1olemmo  10687  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  seq3f1olemstep  10696  seqf1oglem1  10701  seqf1oglem2  10702  fser0const  10717  expaddzaplem  10764  qsqeqor  10832  expnbnd  10845  nn0ltexp2  10891  apexp1  10900  bcval  10931  bccmpl  10936  bcval5  10945  bcpasc  10948  bccl  10949  hashennnuni  10961  hashnncl  10977  fiubm  11010  zfz1isolemiso  11021  lswex  11082  ccatsymb  11096  ccat1st1st  11131  fzowrddc  11138  swrd0g  11151  swrdsbslen  11157  swrdspsleq  11158  pfxclz  11170  pfxwrdsymbg  11181  swrdccatin1  11216  resqrexlemnm  11444  resqrexlemcvg  11445  resqrexlemoverl  11447  resqrexlemglsq  11448  leabs  11500  nn0abscl  11511  ltabs  11513  abslt  11514  fzomaxdif  11539  maxleim  11631  maxabslemval  11634  zmaxcl  11650  2zsupmax  11652  minmax  11656  2zinfmin  11669  xrmaxleim  11670  xrmaxifle  11672  xrmaxiflemab  11673  xrmaxiflemlub  11674  xrmaxiflemcom  11675  xrmaxiflemval  11676  xrmaxaddlem  11686  xrmaxadd  11687  xrminmax  11691  sumdc  11784  sumrbdc  11805  summodclem3  11806  summodclem2a  11807  zsumdc  11810  isumss  11817  fisumss  11818  isumss2  11819  fsumcllem  11825  fsumadd  11832  fsumsplit  11833  fsumsplitsn  11836  sumsplitdc  11858  fisumrev2  11872  fsummulc2  11874  telfsumo  11892  fsumparts  11896  cvgratnnlemseq  11952  cvgratz  11958  fproddccvg  11998  prodrbdc  12000  zproddc  12005  prod1dc  12012  fprodssdc  12016  fprodmul  12017  fprodsplitdc  12022  fprodsplit  12023  fprodunsn  12030  fprodcllem  12032  sinltxirr  12187  fsumdvds  12268  dvdsle  12270  mod2eq1n2dvds  12305  bitsmod  12382  gcdsupex  12393  gcdsupcl  12394  gcdval  12395  gcddvds  12399  gcdcl  12402  gcd0id  12415  gcdneg  12418  bezoutlemmain  12434  bezoutlemzz  12438  bezoutlemaz  12439  bezoutlembz  12440  dfgcd3  12446  dfgcd2  12450  nninfctlemfo  12476  nn0seqcvgd  12478  eucalgf  12492  eucalginv  12493  dvdslcm  12506  lcmcl  12509  lcmneg  12511  lcmgcd  12515  lcmdvds  12516  lcmid  12517  mulgcddvds  12531  isprm5lem  12578  pw2dvdslemn  12602  sqrt2irrap  12617  phibndlem  12653  prm23ge5  12702  pclemdc  12726  pcxqcl  12750  pcge0  12751  pcdvdsb  12758  pceq0  12760  pcneg  12763  pcdvdstr  12765  pcgcd1  12766  pcgcd  12767  pc2dvds  12768  pcz  12770  pcprmpw2  12771  pcaddlem  12777  pcadd  12778  pcmpt  12781  pcmpt2  12782  pcprod  12784  fldivp1  12786  qexpz  12790  1arithlem4  12804  1arith  12805  4sqlem19  12847  ennnfonelemss  12896  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ctiunctlemudc  12923  fvprif  13290  gsumfzz  13442  gsumwsubmcl  13443  gsumwmhm  13445  gsumfzcl  13446  mulgnn0p1  13584  mulgnn0subcl  13586  mulgsubcl  13587  mulgneg  13591  mulgz  13601  mulgnn0dir  13603  mulgdirlem  13604  mulgdir  13605  submmulg  13617  ghmmulg  13707  gsumfzreidx  13788  gsumfzsubmcl  13789  gsumfzmptfidmadd  13790  gsumfzmhm  13794  lringuplu  14073  gsumfzfsum  14465  znf1o  14528  xblss2ps  14991  xblss2  14992  qtopbas  15109  dedekindeulemeu  15209  dedekindeu  15210  suplociccreex  15211  dedekindicclemeu  15218  dedekindicclemicc  15219  limcimolemlt  15251  cnplimclemle  15255  dvmptc  15304  reeff1o  15360  efltlemlt  15361  sin0pilem2  15369  coseq0negpitopi  15423  abssinper  15433  cos02pilt1  15438  logbgcd1irraplemexp  15555  lgslem4  15595  lgsneg  15616  lgsneg1  15617  lgsmod  15618  lgsdilem  15619  lgsdir2  15625  lgsdirprm  15626  lgsdir  15627  lgsdi  15629  lgsne0  15630  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  gausslemma2dlem4  15656  lgseisenlem1  15662  lgsquad3  15676  2sqlem4  15710  2sqlem9  15716  2omap  16132  nnsf  16144  nninfsellemsuc  16151  nnnninfex  16161  trilpolemclim  16177  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  trirec0  16185  apdifflemf  16187  apdifflemr  16188  apdiff  16189  iswomni0  16192  nconstwlpolemgt0  16205  nconstwlpolem  16206  neapmkvlem  16208