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  3570  ifcldadc  3600  ifeq1dadc  3601  ifeq2dadc  3602  ifeqdadc  3603  ifbothdadc  3604  ifcldcd  3608  exmidn0m  4246  exmidsssn  4247  exmidundif  4251  exmidundifim  4252  ordtri2or2exmidlem  4575  reg2exmidlema  4583  nnpredcl  4672  frecabcl  6487  nnsucuniel  6583  dcdifsnid  6592  pw2f1odclem  6933  phpm  6964  fidifsnen  6969  dif1enen  6979  fin0  6984  fimax2gtrilemstep  6999  finexdc  7001  en2eqpr  7006  fientri3  7014  unsnfidcex  7019  unsnfidcel  7020  undifdcss  7022  prfidceq  7027  tpfidceq  7029  fiintim  7030  ssfirab  7035  fidcenumlemrks  7057  fidcenumlemr  7059  omp1eomlem  7198  difinfsnlem  7203  difinfsn  7204  ctssdccl  7215  ctssdc  7217  enumct  7219  nninfninc  7227  nnnninf  7230  nnnninfeq  7232  nnnninfeq2  7233  nninfisol  7237  finomni  7244  ismkvnex  7259  nninfwlpoimlemg  7279  exmidfodomrlemeldju  7309  exmidfodomrlemreseldju  7310  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  exmidaclem  7322  exmidontriimlem3  7337  netap  7368  2omotaplemap  7371  mullocprlem  7685  recexprlemloc  7746  suplocsrlem  7923  btwnapz  9505  xnn0dcle  9926  xnn0letri  9927  z2ge  9950  xaddcom  9985  xnegdi  9992  xaddass  9993  xpncan  9995  xleadd1a  9997  xsubge0  10005  xlesubadd  10007  fztri3or  10163  fzm1  10224  fzneuz  10225  exfzdc  10371  zsupcllemstep  10374  infssuzex  10378  exbtwnzlemstep  10392  rebtwn2zlemstep  10397  xqltnle  10412  apbtwnz  10419  modifeq2int  10533  modsumfzodifsn  10543  iseqf1olemab  10649  iseqf1olemmo  10652  seq3f1olemqsumk  10659  seq3f1olemqsum  10660  seq3f1olemstep  10661  seqf1oglem1  10666  seqf1oglem2  10667  fser0const  10682  expaddzaplem  10729  qsqeqor  10797  expnbnd  10810  nn0ltexp2  10856  apexp1  10865  bcval  10896  bccmpl  10901  bcval5  10910  bcpasc  10913  bccl  10914  hashennnuni  10926  hashnncl  10942  fiubm  10975  zfz1isolemiso  10986  lswex  11047  ccatsymb  11061  ccat1st1st  11096  fzowrddc  11103  swrd0g  11116  swrdsbslen  11122  swrdspsleq  11123  pfxwrdsymbg  11144  resqrexlemnm  11362  resqrexlemcvg  11363  resqrexlemoverl  11365  resqrexlemglsq  11366  leabs  11418  nn0abscl  11429  ltabs  11431  abslt  11432  fzomaxdif  11457  maxleim  11549  maxabslemval  11552  zmaxcl  11568  2zsupmax  11570  minmax  11574  2zinfmin  11587  xrmaxleim  11588  xrmaxifle  11590  xrmaxiflemab  11591  xrmaxiflemlub  11592  xrmaxiflemcom  11593  xrmaxiflemval  11594  xrmaxaddlem  11604  xrmaxadd  11605  xrminmax  11609  sumdc  11702  sumrbdc  11723  summodclem3  11724  summodclem2a  11725  zsumdc  11728  isumss  11735  fisumss  11736  isumss2  11737  fsumcllem  11743  fsumadd  11750  fsumsplit  11751  fsumsplitsn  11754  sumsplitdc  11776  fisumrev2  11790  fsummulc2  11792  telfsumo  11810  fsumparts  11814  cvgratnnlemseq  11870  cvgratz  11876  fproddccvg  11916  prodrbdc  11918  zproddc  11923  prod1dc  11930  fprodssdc  11934  fprodmul  11935  fprodsplitdc  11940  fprodsplit  11941  fprodunsn  11948  fprodcllem  11950  sinltxirr  12105  fsumdvds  12186  dvdsle  12188  mod2eq1n2dvds  12223  bitsmod  12300  gcdsupex  12311  gcdsupcl  12312  gcdval  12313  gcddvds  12317  gcdcl  12320  gcd0id  12333  gcdneg  12336  bezoutlemmain  12352  bezoutlemzz  12356  bezoutlemaz  12357  bezoutlembz  12358  dfgcd3  12364  dfgcd2  12368  nninfctlemfo  12394  nn0seqcvgd  12396  eucalgf  12410  eucalginv  12411  dvdslcm  12424  lcmcl  12427  lcmneg  12429  lcmgcd  12433  lcmdvds  12434  lcmid  12435  mulgcddvds  12449  isprm5lem  12496  pw2dvdslemn  12520  sqrt2irrap  12535  phibndlem  12571  prm23ge5  12620  pclemdc  12644  pcxqcl  12668  pcge0  12669  pcdvdsb  12676  pceq0  12678  pcneg  12681  pcdvdstr  12683  pcgcd1  12684  pcgcd  12685  pc2dvds  12686  pcz  12688  pcprmpw2  12689  pcaddlem  12695  pcadd  12696  pcmpt  12699  pcmpt2  12700  pcprod  12702  fldivp1  12704  qexpz  12708  1arithlem4  12722  1arith  12723  4sqlem19  12765  ennnfonelemss  12814  ennnfonelemkh  12816  ennnfonelemhf1o  12817  ctiunctlemudc  12841  fvprif  13208  gsumfzz  13360  gsumwsubmcl  13361  gsumwmhm  13363  gsumfzcl  13364  mulgnn0p1  13502  mulgnn0subcl  13504  mulgsubcl  13505  mulgneg  13509  mulgz  13519  mulgnn0dir  13521  mulgdirlem  13522  mulgdir  13523  submmulg  13535  ghmmulg  13625  gsumfzreidx  13706  gsumfzsubmcl  13707  gsumfzmptfidmadd  13708  gsumfzmhm  13712  lringuplu  13991  gsumfzfsum  14383  znf1o  14446  xblss2ps  14909  xblss2  14910  qtopbas  15027  dedekindeulemeu  15127  dedekindeu  15128  suplociccreex  15129  dedekindicclemeu  15136  dedekindicclemicc  15137  limcimolemlt  15169  cnplimclemle  15173  dvmptc  15222  reeff1o  15278  efltlemlt  15279  sin0pilem2  15287  coseq0negpitopi  15341  abssinper  15351  cos02pilt1  15356  logbgcd1irraplemexp  15473  lgslem4  15513  lgsneg  15534  lgsneg1  15535  lgsmod  15536  lgsdilem  15537  lgsdir2  15543  lgsdirprm  15544  lgsdir  15545  lgsdi  15547  lgsne0  15548  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem1a  15568  gausslemma2dlem1f1o  15570  gausslemma2dlem4  15574  lgseisenlem1  15580  lgsquad3  15594  2sqlem4  15628  2sqlem9  15634  2omap  15969  nnsf  15979  nninfsellemsuc  15986  nnnninfex  15996  trilpolemclim  16012  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  trirec0  16020  apdifflemf  16022  apdifflemr  16023  apdiff  16024  iswomni0  16027  nconstwlpolemgt0  16040  nconstwlpolem  16041  neapmkvlem  16043