Theorem mpjaodan 798

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1307  dcun  3533  ifcldadc  3563  ifeq1dadc  3564  ifeq2dadc  3565  ifbothdadc  3566  ifcldcd  3570  exmidn0m  4199  exmidsssn  4200  exmidundif  4204  exmidundifim  4205  ordtri2or2exmidlem  4523  reg2exmidlema  4531  nnpredcl  4620  frecabcl  6395  nnsucuniel  6491  dcdifsnid  6500  phpm  6860  fidifsnen  6865  dif1enen  6875  fin0  6880  fimax2gtrilemstep  6895  finexdc  6897  en2eqpr  6902  fientri3  6909  unsnfidcex  6914  unsnfidcel  6915  undifdcss  6917  fiintim  6923  ssfirab  6928  fidcenumlemrks  6947  fidcenumlemr  6949  omp1eomlem  7088  difinfsnlem  7093  difinfsn  7094  ctssdccl  7105  ctssdc  7107  enumct  7109  nnnninf  7119  nnnninfeq  7121  nnnninfeq2  7122  nninfisol  7126  finomni  7133  ismkvnex  7148  nninfwlpoimlemg  7168  exmidfodomrlemeldju  7193  exmidfodomrlemreseldju  7194  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  exmidaclem  7202  exmidontriimlem3  7217  netap  7248  2omotaplemap  7251  mullocprlem  7564  recexprlemloc  7625  suplocsrlem  7802  btwnapz  9377  xnn0dcle  9796  xnn0letri  9797  z2ge  9820  xaddcom  9855  xnegdi  9862  xaddass  9863  xpncan  9865  xleadd1a  9867  xsubge0  9875  xlesubadd  9877  fztri3or  10032  fzm1  10093  fzneuz  10094  exfzdc  10233  exbtwnzlemstep  10241  rebtwn2zlemstep  10246  apbtwnz  10267  modifeq2int  10379  modsumfzodifsn  10389  iseqf1olemab  10482  iseqf1olemmo  10485  seq3f1olemqsumk  10492  seq3f1olemqsum  10493  seq3f1olemstep  10494  fser0const  10509  expaddzaplem  10556  qsqeqor  10623  expnbnd  10636  nn0ltexp2  10681  apexp1  10689  bcval  10720  bccmpl  10725  bcval5  10734  bcpasc  10737  bccl  10738  hashennnuni  10750  hashnncl  10766  fiubm  10799  zfz1isolemiso  10810  resqrexlemnm  11018  resqrexlemcvg  11019  resqrexlemoverl  11021  resqrexlemglsq  11022  leabs  11074  nn0abscl  11085  ltabs  11087  abslt  11088  fzomaxdif  11113  maxleim  11205  maxabslemval  11208  zmaxcl  11224  2zsupmax  11225  minmax  11229  2zinfmin  11242  xrmaxleim  11243  xrmaxifle  11245  xrmaxiflemab  11246  xrmaxiflemlub  11247  xrmaxiflemcom  11248  xrmaxiflemval  11249  xrmaxaddlem  11259  xrmaxadd  11260  xrminmax  11264  sumdc  11357  sumrbdc  11378  summodclem3  11379  summodclem2a  11380  zsumdc  11383  isumss  11390  fisumss  11391  isumss2  11392  fsumcllem  11398  fsumadd  11405  fsumsplit  11406  fsumsplitsn  11409  sumsplitdc  11431  fisumrev2  11445  fsummulc2  11447  telfsumo  11465  fsumparts  11469  cvgratnnlemseq  11525  cvgratz  11531  fproddccvg  11571  prodrbdc  11573  zproddc  11578  prod1dc  11585  fprodssdc  11589  fprodmul  11590  fprodsplitdc  11595  fprodsplit  11596  fprodunsn  11603  fprodcllem  11605  dvdsle  11840  mod2eq1n2dvds  11874  zsupcllemstep  11936  infssuzex  11940  gcdsupex  11948  gcdsupcl  11949  gcdval  11950  gcddvds  11954  gcdcl  11957  gcd0id  11970  gcdneg  11973  bezoutlemmain  11989  bezoutlemzz  11993  bezoutlemaz  11994  bezoutlembz  11995  dfgcd3  12001  dfgcd2  12005  nn0seqcvgd  12031  eucalgf  12045  eucalginv  12046  dvdslcm  12059  lcmcl  12062  lcmneg  12064  lcmgcd  12068  lcmdvds  12069  lcmid  12070  mulgcddvds  12084  isprm5lem  12131  pw2dvdslemn  12155  sqrt2irrap  12170  phibndlem  12206  prm23ge5  12254  pclemdc  12278  pcge0  12302  pcdvdsb  12309  pceq0  12311  pcneg  12314  pcdvdstr  12316  pcgcd1  12317  pcgcd  12318  pc2dvds  12319  pcz  12321  pcprmpw2  12322  pcaddlem  12328  pcadd  12329  pcmpt  12331  pcmpt2  12332  pcprod  12334  fldivp1  12336  qexpz  12340  1arithlem4  12354  1arith  12355  ennnfonelemss  12401  ennnfonelemkh  12403  ennnfonelemhf1o  12404  ctiunctlemudc  12428  mulgnn0p1  12922  mulgnn0subcl  12924  mulgsubcl  12925  mulgneg  12929  mulgz  12938  mulgnn0dir  12940  mulgdirlem  12941  mulgdir  12942  lringuplu  13236  xblss2ps  13686  xblss2  13687  qtopbas  13804  dedekindeulemeu  13882  dedekindeu  13883  suplociccreex  13884  dedekindicclemeu  13891  dedekindicclemicc  13892  limcimolemlt  13915  cnplimclemle  13919  reeff1o  13976  efltlemlt  13977  sin0pilem2  13985  coseq0negpitopi  14039  abssinper  14049  cos02pilt1  14054  logbgcd1irraplemexp  14168  lgslem4  14186  lgsneg  14207  lgsneg1  14208  lgsmod  14209  lgsdilem  14210  lgsdir2  14216  lgsdirprm  14217  lgsdir  14218  lgsdi  14220  lgsne0  14221  lgsdirnn0  14230  lgsdinn0  14231  2sqlem4  14236  2sqlem9  14242  nnsf  14525  nninfsellemsuc  14532  trilpolemclim  14555  trilpolemisumle  14557  trilpolemeq1  14559  trilpolemlt1  14560  trirec0  14563  apdifflemf  14565  apdifflemr  14566  apdiff  14567  iswomni0  14570  nconstwlpolemgt0  14582  nconstwlpolem  14583  neapmkvlem  14585