Theorem mpjaodan 805

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1343  dcun  3604  ifcldadc  3635  ifeq1dadc  3636  ifeq2dadc  3637  ifeqdadc  3638  ifbothdadc  3639  ifcldcd  3643  2if2dc  3645  exmidn0m  4291  exmidsssn  4292  exmidundif  4296  exmidundifim  4297  ordtri2or2exmidlem  4624  reg2exmidlema  4632  nnpredcl  4721  frecabcl  6565  nnsucuniel  6663  dcdifsnid  6672  pw2f1odclem  7020  phpm  7052  fidifsnen  7057  dif1enen  7069  fin0  7074  fimax2gtrilemstep  7090  finexdc  7092  elssdc  7094  eqsndc  7095  en2eqpr  7099  fientri3  7107  unsnfidcex  7112  unsnfidcel  7113  undifdcss  7115  prfidceq  7120  tpfidceq  7122  fiintim  7123  ssfirab  7129  fidcenumlemrks  7152  fidcenumlemr  7154  omp1eomlem  7293  difinfsnlem  7298  difinfsn  7299  ctssdccl  7310  ctssdc  7312  enumct  7314  nninfninc  7322  nnnninf  7325  nnnninfeq  7327  nnnninfeq2  7328  nninfisol  7332  finomni  7339  ismkvnex  7354  nninfwlpoimlemg  7374  pr2cv1  7400  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  exmidontriimlem3  7438  netap  7473  2omotaplemap  7476  mullocprlem  7790  recexprlemloc  7851  suplocsrlem  8028  btwnapz  9610  xnn0dcle  10037  xnn0letri  10038  z2ge  10061  xaddcom  10096  xnegdi  10103  xaddass  10104  xpncan  10106  xleadd1a  10108  xsubge0  10116  xlesubadd  10118  fztri3or  10274  fzm1  10335  fzneuz  10336  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  xqltnle  10528  apbtwnz  10535  modifeq2int  10649  modsumfzodifsn  10659  iseqf1olemab  10765  iseqf1olemmo  10768  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemstep  10777  seqf1oglem1  10782  seqf1oglem2  10783  fser0const  10798  expaddzaplem  10845  qsqeqor  10913  expnbnd  10926  nn0ltexp2  10972  apexp1  10981  bcval  11012  bccmpl  11017  bcval5  11026  bcpasc  11029  bccl  11030  hashennnuni  11042  hashnncl  11058  fiubm  11093  zfz1isolemiso  11104  lswex  11169  ccatsymb  11183  ccat1st1st  11222  fzowrddc  11232  swrd0g  11245  swrdsbslen  11251  swrdspsleq  11252  pfxclz  11264  pfxwrdsymbg  11275  swrdccatin1  11310  resqrexlemnm  11596  resqrexlemcvg  11597  resqrexlemoverl  11599  resqrexlemglsq  11600  leabs  11652  nn0abscl  11663  ltabs  11665  abslt  11666  fzomaxdif  11691  maxleim  11783  maxabslemval  11786  zmaxcl  11802  2zsupmax  11804  minmax  11808  2zinfmin  11821  xrmaxleim  11822  xrmaxifle  11824  xrmaxiflemab  11825  xrmaxiflemlub  11826  xrmaxiflemcom  11827  xrmaxiflemval  11828  xrmaxaddlem  11838  xrmaxadd  11839  xrminmax  11843  sumdc  11936  fzf1o  11954  sumrbdc  11958  summodclem3  11959  summodclem2a  11960  zsumdc  11963  isumss  11970  fisumss  11971  isumss2  11972  fsumcllem  11978  fsumadd  11985  fsumsplit  11986  fsumsplitsn  11989  sumsplitdc  12011  fisumrev2  12025  fsummulc2  12027  telfsumo  12045  fsumparts  12049  cvgratnnlemseq  12105  cvgratz  12111  fproddccvg  12151  prodrbdc  12153  zproddc  12158  prod1dc  12165  fprodssdc  12169  fprodmul  12170  fprodsplitdc  12175  fprodsplit  12176  fprodunsn  12183  fprodcllem  12185  sinltxirr  12340  fsumdvds  12421  dvdsle  12423  mod2eq1n2dvds  12458  bitsmod  12535  gcdsupex  12546  gcdsupcl  12547  gcdval  12548  gcddvds  12552  gcdcl  12555  gcd0id  12568  gcdneg  12571  bezoutlemmain  12587  bezoutlemzz  12591  bezoutlemaz  12592  bezoutlembz  12593  dfgcd3  12599  dfgcd2  12603  nninfctlemfo  12629  nn0seqcvgd  12631  eucalgf  12645  eucalginv  12646  dvdslcm  12659  lcmcl  12662  lcmneg  12664  lcmgcd  12668  lcmdvds  12669  lcmid  12670  mulgcddvds  12684  isprm5lem  12731  pw2dvdslemn  12755  sqrt2irrap  12770  phibndlem  12806  prm23ge5  12855  pclemdc  12879  pcxqcl  12903  pcge0  12904  pcdvdsb  12911  pceq0  12913  pcneg  12916  pcdvdstr  12918  pcgcd1  12919  pcgcd  12920  pc2dvds  12921  pcz  12923  pcprmpw2  12924  pcaddlem  12930  pcadd  12931  pcmpt  12934  pcmpt2  12935  pcprod  12937  fldivp1  12939  qexpz  12943  1arithlem4  12957  1arith  12958  4sqlem19  13000  ennnfonelemss  13049  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ctiunctlemudc  13076  bassetsnn  13157  fvprif  13444  gsumfzz  13596  gsumwsubmcl  13597  gsumwmhm  13599  gsumfzcl  13600  mulgnn0p1  13738  mulgnn0subcl  13740  mulgsubcl  13741  mulgneg  13745  mulgz  13755  mulgnn0dir  13757  mulgdirlem  13758  mulgdir  13759  submmulg  13771  ghmmulg  13861  gsumfzreidx  13942  gsumfzsubmcl  13943  gsumfzmptfidmadd  13944  gsumfzmhm  13948  gsumsplit0  13951  lringuplu  14229  gsumfzfsum  14621  znf1o  14684  xblss2ps  15147  xblss2  15148  qtopbas  15265  dedekindeulemeu  15365  dedekindeu  15366  suplociccreex  15367  dedekindicclemeu  15374  dedekindicclemicc  15375  limcimolemlt  15407  cnplimclemle  15411  dvmptc  15460  reeff1o  15516  efltlemlt  15517  sin0pilem2  15525  coseq0negpitopi  15579  abssinper  15589  cos02pilt1  15594  logbgcd1irraplemexp  15711  lgslem4  15751  lgsneg  15772  lgsneg1  15773  lgsmod  15774  lgsdilem  15775  lgsdir2  15781  lgsdirprm  15782  lgsdir  15783  lgsdi  15785  lgsne0  15786  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem4  15812  lgseisenlem1  15818  lgsquad3  15832  2sqlem4  15866  2sqlem9  15872  eupth2lem3lem3fi  16340  eupth2lem3lem4fi  16343  eupth2lem3lem7fi  16344  2omap  16645  nnsf  16658  nninfsellemsuc  16665  nnnninfex  16675  trilpolemclim  16691  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  trirec0  16699  apdifflemf  16701  apdifflemr  16702  apdiff  16703  iswomni0  16707  nconstwlpolemgt0  16720  nconstwlpolem  16721  neapmkvlem  16723  gfsumval  16732  gsumgfsum  16736