Theorem mpjaodan 799

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1318  dcun  3561  ifcldadc  3591  ifeq1dadc  3592  ifeq2dadc  3593  ifbothdadc  3594  ifcldcd  3598  exmidn0m  4235  exmidsssn  4236  exmidundif  4240  exmidundifim  4241  ordtri2or2exmidlem  4563  reg2exmidlema  4571  nnpredcl  4660  frecabcl  6466  nnsucuniel  6562  dcdifsnid  6571  pw2f1odclem  6904  phpm  6935  fidifsnen  6940  dif1enen  6950  fin0  6955  fimax2gtrilemstep  6970  finexdc  6972  en2eqpr  6977  fientri3  6985  unsnfidcex  6990  unsnfidcel  6991  undifdcss  6993  prfidceq  6998  tpfidceq  7000  fiintim  7001  ssfirab  7006  fidcenumlemrks  7028  fidcenumlemr  7030  omp1eomlem  7169  difinfsnlem  7174  difinfsn  7175  ctssdccl  7186  ctssdc  7188  enumct  7190  nninfninc  7198  nnnninf  7201  nnnninfeq  7203  nnnninfeq2  7204  nninfisol  7208  finomni  7215  ismkvnex  7230  nninfwlpoimlemg  7250  exmidfodomrlemeldju  7278  exmidfodomrlemreseldju  7279  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  exmidaclem  7291  exmidontriimlem3  7306  netap  7337  2omotaplemap  7340  mullocprlem  7654  recexprlemloc  7715  suplocsrlem  7892  btwnapz  9473  xnn0dcle  9894  xnn0letri  9895  z2ge  9918  xaddcom  9953  xnegdi  9960  xaddass  9961  xpncan  9963  xleadd1a  9965  xsubge0  9973  xlesubadd  9975  fztri3or  10131  fzm1  10192  fzneuz  10193  exfzdc  10333  zsupcllemstep  10336  infssuzex  10340  exbtwnzlemstep  10354  rebtwn2zlemstep  10359  xqltnle  10374  apbtwnz  10381  modifeq2int  10495  modsumfzodifsn  10505  iseqf1olemab  10611  iseqf1olemmo  10614  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seq3f1olemstep  10623  seqf1oglem1  10628  seqf1oglem2  10629  fser0const  10644  expaddzaplem  10691  qsqeqor  10759  expnbnd  10772  nn0ltexp2  10818  apexp1  10827  bcval  10858  bccmpl  10863  bcval5  10872  bcpasc  10875  bccl  10876  hashennnuni  10888  hashnncl  10904  fiubm  10937  zfz1isolemiso  10948  resqrexlemnm  11200  resqrexlemcvg  11201  resqrexlemoverl  11203  resqrexlemglsq  11204  leabs  11256  nn0abscl  11267  ltabs  11269  abslt  11270  fzomaxdif  11295  maxleim  11387  maxabslemval  11390  zmaxcl  11406  2zsupmax  11408  minmax  11412  2zinfmin  11425  xrmaxleim  11426  xrmaxifle  11428  xrmaxiflemab  11429  xrmaxiflemlub  11430  xrmaxiflemcom  11431  xrmaxiflemval  11432  xrmaxaddlem  11442  xrmaxadd  11443  xrminmax  11447  sumdc  11540  sumrbdc  11561  summodclem3  11562  summodclem2a  11563  zsumdc  11566  isumss  11573  fisumss  11574  isumss2  11575  fsumcllem  11581  fsumadd  11588  fsumsplit  11589  fsumsplitsn  11592  sumsplitdc  11614  fisumrev2  11628  fsummulc2  11630  telfsumo  11648  fsumparts  11652  cvgratnnlemseq  11708  cvgratz  11714  fproddccvg  11754  prodrbdc  11756  zproddc  11761  prod1dc  11768  fprodssdc  11772  fprodmul  11773  fprodsplitdc  11778  fprodsplit  11779  fprodunsn  11786  fprodcllem  11788  sinltxirr  11943  fsumdvds  12024  dvdsle  12026  mod2eq1n2dvds  12061  bitsmod  12138  gcdsupex  12149  gcdsupcl  12150  gcdval  12151  gcddvds  12155  gcdcl  12158  gcd0id  12171  gcdneg  12174  bezoutlemmain  12190  bezoutlemzz  12194  bezoutlemaz  12195  bezoutlembz  12196  dfgcd3  12202  dfgcd2  12206  nninfctlemfo  12232  nn0seqcvgd  12234  eucalgf  12248  eucalginv  12249  dvdslcm  12262  lcmcl  12265  lcmneg  12267  lcmgcd  12271  lcmdvds  12272  lcmid  12273  mulgcddvds  12287  isprm5lem  12334  pw2dvdslemn  12358  sqrt2irrap  12373  phibndlem  12409  prm23ge5  12458  pclemdc  12482  pcxqcl  12506  pcge0  12507  pcdvdsb  12514  pceq0  12516  pcneg  12519  pcdvdstr  12521  pcgcd1  12522  pcgcd  12523  pc2dvds  12524  pcz  12526  pcprmpw2  12527  pcaddlem  12533  pcadd  12534  pcmpt  12537  pcmpt2  12538  pcprod  12540  fldivp1  12542  qexpz  12546  1arithlem4  12560  1arith  12561  4sqlem19  12603  ennnfonelemss  12652  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ctiunctlemudc  12679  fvprif  13045  gsumfzz  13197  gsumwsubmcl  13198  gsumwmhm  13200  gsumfzcl  13201  mulgnn0p1  13339  mulgnn0subcl  13341  mulgsubcl  13342  mulgneg  13346  mulgz  13356  mulgnn0dir  13358  mulgdirlem  13359  mulgdir  13360  submmulg  13372  ghmmulg  13462  gsumfzreidx  13543  gsumfzsubmcl  13544  gsumfzmptfidmadd  13545  gsumfzmhm  13549  lringuplu  13828  gsumfzfsum  14220  znf1o  14283  xblss2ps  14724  xblss2  14725  qtopbas  14842  dedekindeulemeu  14942  dedekindeu  14943  suplociccreex  14944  dedekindicclemeu  14951  dedekindicclemicc  14952  limcimolemlt  14984  cnplimclemle  14988  dvmptc  15037  reeff1o  15093  efltlemlt  15094  sin0pilem2  15102  coseq0negpitopi  15156  abssinper  15166  cos02pilt1  15171  logbgcd1irraplemexp  15288  lgslem4  15328  lgsneg  15349  lgsneg1  15350  lgsmod  15351  lgsdilem  15352  lgsdir2  15358  lgsdirprm  15359  lgsdir  15360  lgsdi  15362  lgsne0  15363  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem4  15389  lgseisenlem1  15395  lgsquad3  15409  2sqlem4  15443  2sqlem9  15449  2omap  15726  nnsf  15736  nninfsellemsuc  15743  trilpolemclim  15767  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  trirec0  15775  apdifflemf  15777  apdifflemr  15778  apdiff  15779  iswomni0  15782  nconstwlpolemgt0  15795  nconstwlpolem  15796  neapmkvlem  15798