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  3548  ifcldadc  3578  ifeq1dadc  3579  ifeq2dadc  3580  ifbothdadc  3581  ifcldcd  3585  exmidn0m  4219  exmidsssn  4220  exmidundif  4224  exmidundifim  4225  ordtri2or2exmidlem  4543  reg2exmidlema  4551  nnpredcl  4640  frecabcl  6424  nnsucuniel  6520  dcdifsnid  6529  pw2f1odclem  6862  phpm  6893  fidifsnen  6898  dif1enen  6908  fin0  6913  fimax2gtrilemstep  6928  finexdc  6930  en2eqpr  6935  fientri3  6943  unsnfidcex  6948  unsnfidcel  6949  undifdcss  6951  fiintim  6957  ssfirab  6962  fidcenumlemrks  6982  fidcenumlemr  6984  omp1eomlem  7123  difinfsnlem  7128  difinfsn  7129  ctssdccl  7140  ctssdc  7142  enumct  7144  nnnninf  7154  nnnninfeq  7156  nnnninfeq2  7157  nninfisol  7161  finomni  7168  ismkvnex  7183  nninfwlpoimlemg  7203  exmidfodomrlemeldju  7228  exmidfodomrlemreseldju  7229  exmidfodomrlemr  7231  exmidfodomrlemrALT  7232  exmidaclem  7237  exmidontriimlem3  7252  netap  7283  2omotaplemap  7286  mullocprlem  7599  recexprlemloc  7660  suplocsrlem  7837  btwnapz  9413  xnn0dcle  9832  xnn0letri  9833  z2ge  9856  xaddcom  9891  xnegdi  9898  xaddass  9899  xpncan  9901  xleadd1a  9903  xsubge0  9911  xlesubadd  9913  fztri3or  10069  fzm1  10130  fzneuz  10131  exfzdc  10270  exbtwnzlemstep  10278  rebtwn2zlemstep  10283  xqltnle  10298  apbtwnz  10305  modifeq2int  10417  modsumfzodifsn  10427  iseqf1olemab  10520  iseqf1olemmo  10523  seq3f1olemqsumk  10530  seq3f1olemqsum  10531  seq3f1olemstep  10532  fser0const  10547  expaddzaplem  10594  qsqeqor  10662  expnbnd  10675  nn0ltexp2  10721  apexp1  10730  bcval  10761  bccmpl  10766  bcval5  10775  bcpasc  10778  bccl  10779  hashennnuni  10791  hashnncl  10807  fiubm  10840  zfz1isolemiso  10851  resqrexlemnm  11059  resqrexlemcvg  11060  resqrexlemoverl  11062  resqrexlemglsq  11063  leabs  11115  nn0abscl  11126  ltabs  11128  abslt  11129  fzomaxdif  11154  maxleim  11246  maxabslemval  11249  zmaxcl  11265  2zsupmax  11266  minmax  11270  2zinfmin  11283  xrmaxleim  11284  xrmaxifle  11286  xrmaxiflemab  11287  xrmaxiflemlub  11288  xrmaxiflemcom  11289  xrmaxiflemval  11290  xrmaxaddlem  11300  xrmaxadd  11301  xrminmax  11305  sumdc  11398  sumrbdc  11419  summodclem3  11420  summodclem2a  11421  zsumdc  11424  isumss  11431  fisumss  11432  isumss2  11433  fsumcllem  11439  fsumadd  11446  fsumsplit  11447  fsumsplitsn  11450  sumsplitdc  11472  fisumrev2  11486  fsummulc2  11488  telfsumo  11506  fsumparts  11510  cvgratnnlemseq  11566  cvgratz  11572  fproddccvg  11612  prodrbdc  11614  zproddc  11619  prod1dc  11626  fprodssdc  11630  fprodmul  11631  fprodsplitdc  11636  fprodsplit  11637  fprodunsn  11644  fprodcllem  11646  dvdsle  11882  mod2eq1n2dvds  11916  zsupcllemstep  11978  infssuzex  11982  gcdsupex  11990  gcdsupcl  11991  gcdval  11992  gcddvds  11996  gcdcl  11999  gcd0id  12012  gcdneg  12015  bezoutlemmain  12031  bezoutlemzz  12035  bezoutlemaz  12036  bezoutlembz  12037  dfgcd3  12043  dfgcd2  12047  nn0seqcvgd  12073  eucalgf  12087  eucalginv  12088  dvdslcm  12101  lcmcl  12104  lcmneg  12106  lcmgcd  12110  lcmdvds  12111  lcmid  12112  mulgcddvds  12126  isprm5lem  12173  pw2dvdslemn  12197  sqrt2irrap  12212  phibndlem  12248  prm23ge5  12296  pclemdc  12320  pcxqcl  12344  pcge0  12345  pcdvdsb  12352  pceq0  12354  pcneg  12357  pcdvdstr  12359  pcgcd1  12360  pcgcd  12361  pc2dvds  12362  pcz  12364  pcprmpw2  12365  pcaddlem  12371  pcadd  12372  pcmpt  12375  pcmpt2  12376  pcprod  12378  fldivp1  12380  qexpz  12384  1arithlem4  12398  1arith  12399  4sqlem19  12441  ennnfonelemss  12461  ennnfonelemkh  12463  ennnfonelemhf1o  12464  ctiunctlemudc  12488  fvprif  12819  mulgnn0p1  13073  mulgnn0subcl  13075  mulgsubcl  13076  mulgneg  13080  mulgz  13090  mulgnn0dir  13092  mulgdirlem  13093  mulgdir  13094  ghmmulg  13195  lringuplu  13543  xblss2ps  14361  xblss2  14362  qtopbas  14479  dedekindeulemeu  14557  dedekindeu  14558  suplociccreex  14559  dedekindicclemeu  14566  dedekindicclemicc  14567  limcimolemlt  14590  cnplimclemle  14594  reeff1o  14651  efltlemlt  14652  sin0pilem2  14660  coseq0negpitopi  14714  abssinper  14724  cos02pilt1  14729  logbgcd1irraplemexp  14843  lgslem4  14862  lgsneg  14883  lgsneg1  14884  lgsmod  14885  lgsdilem  14886  lgsdir2  14892  lgsdirprm  14893  lgsdir  14894  lgsdi  14896  lgsne0  14897  lgsdirnn0  14906  lgsdinn0  14907  lgseisenlem1  14908  2sqlem4  14923  2sqlem9  14929  nnsf  15213  nninfsellemsuc  15220  trilpolemclim  15243  trilpolemisumle  15245  trilpolemeq1  15247  trilpolemlt1  15248  trirec0  15251  apdifflemf  15253  apdifflemr  15254  apdiff  15255  iswomni0  15258  nconstwlpolemgt0  15271  nconstwlpolem  15272  neapmkvlem  15274