Theorem mpjaodan 788

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

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjao3dan  1297  dcun  3519  ifcldadc  3549  ifeq1dadc  3550  ifbothdadc  3551  ifcldcd  3555  exmidn0m  4180  exmidsssn  4181  exmidundif  4185  exmidundifim  4186  ordtri2or2exmidlem  4503  reg2exmidlema  4511  nnpredcl  4600  frecabcl  6367  nnsucuniel  6463  dcdifsnid  6472  phpm  6831  fidifsnen  6836  dif1enen  6846  fin0  6851  fimax2gtrilemstep  6866  finexdc  6868  en2eqpr  6873  fientri3  6880  unsnfidcex  6885  unsnfidcel  6886  undifdcss  6888  fiintim  6894  ssfirab  6899  fidcenumlemrks  6918  fidcenumlemr  6920  omp1eomlem  7059  difinfsnlem  7064  difinfsn  7065  ctssdccl  7076  ctssdc  7078  enumct  7080  nnnninf  7090  nnnninfeq  7092  nnnninfeq2  7093  nninfisol  7097  finomni  7104  ismkvnex  7119  exmidfodomrlemeldju  7155  exmidfodomrlemreseldju  7156  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  exmidontriimlem3  7179  mullocprlem  7511  recexprlemloc  7572  suplocsrlem  7749  btwnapz  9321  xnn0dcle  9738  xnn0letri  9739  z2ge  9762  xaddcom  9797  xnegdi  9804  xaddass  9805  xpncan  9807  xleadd1a  9809  xsubge0  9817  xlesubadd  9819  fztri3or  9974  fzm1  10035  fzneuz  10036  exfzdc  10175  exbtwnzlemstep  10183  rebtwn2zlemstep  10188  apbtwnz  10209  modifeq2int  10321  modsumfzodifsn  10331  iseqf1olemab  10424  iseqf1olemmo  10427  seq3f1olemqsumk  10434  seq3f1olemqsum  10435  seq3f1olemstep  10436  fser0const  10451  expaddzaplem  10498  qsqeqor  10565  expnbnd  10578  nn0ltexp2  10623  apexp1  10631  bcval  10662  bccmpl  10667  bcval5  10676  bcpasc  10679  bccl  10680  hashennnuni  10692  hashnncl  10709  fiubm  10741  zfz1isolemiso  10752  resqrexlemnm  10960  resqrexlemcvg  10961  resqrexlemoverl  10963  resqrexlemglsq  10964  leabs  11016  nn0abscl  11027  ltabs  11029  abslt  11030  fzomaxdif  11055  maxleim  11147  maxabslemval  11150  zmaxcl  11166  2zsupmax  11167  minmax  11171  2zinfmin  11184  xrmaxleim  11185  xrmaxifle  11187  xrmaxiflemab  11188  xrmaxiflemlub  11189  xrmaxiflemcom  11190  xrmaxiflemval  11191  xrmaxaddlem  11201  xrmaxadd  11202  xrminmax  11206  sumdc  11299  sumrbdc  11320  summodclem3  11321  summodclem2a  11322  zsumdc  11325  isumss  11332  fisumss  11333  isumss2  11334  fsumcllem  11340  fsumadd  11347  fsumsplit  11348  fsumsplitsn  11351  sumsplitdc  11373  fisumrev2  11387  fsummulc2  11389  telfsumo  11407  fsumparts  11411  cvgratnnlemseq  11467  cvgratz  11473  fproddccvg  11513  prodrbdc  11515  zproddc  11520  prod1dc  11527  fprodssdc  11531  fprodmul  11532  fprodsplitdc  11537  fprodsplit  11538  fprodunsn  11545  fprodcllem  11547  dvdsle  11782  mod2eq1n2dvds  11816  zsupcllemstep  11878  infssuzex  11882  gcdsupex  11890  gcdsupcl  11891  gcdval  11892  gcddvds  11896  gcdcl  11899  gcd0id  11912  gcdneg  11915  bezoutlemmain  11931  bezoutlemzz  11935  bezoutlemaz  11936  bezoutlembz  11937  dfgcd3  11943  dfgcd2  11947  nn0seqcvgd  11973  eucalgf  11987  eucalginv  11988  dvdslcm  12001  lcmcl  12004  lcmneg  12006  lcmgcd  12010  lcmdvds  12011  lcmid  12012  mulgcddvds  12026  isprm5lem  12073  pw2dvdslemn  12097  sqrt2irrap  12112  phibndlem  12148  prm23ge5  12196  pclemdc  12220  pcge0  12244  pcdvdsb  12251  pceq0  12253  pcneg  12256  pcdvdstr  12258  pcgcd1  12259  pcgcd  12260  pc2dvds  12261  pcz  12263  pcprmpw2  12264  pcaddlem  12270  pcadd  12271  pcmpt  12273  pcmpt2  12274  pcprod  12276  fldivp1  12278  qexpz  12282  1arithlem4  12296  1arith  12297  ennnfonelemss  12343  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ctiunctlemudc  12370  xblss2ps  13044  xblss2  13045  qtopbas  13162  dedekindeulemeu  13240  dedekindeu  13241  suplociccreex  13242  dedekindicclemeu  13249  dedekindicclemicc  13250  limcimolemlt  13273  cnplimclemle  13277  reeff1o  13334  efltlemlt  13335  sin0pilem2  13343  coseq0negpitopi  13397  abssinper  13407  cos02pilt1  13412  logbgcd1irraplemexp  13526  lgslem4  13544  lgsneg  13565  lgsneg1  13566  lgsmod  13567  lgsdilem  13568  lgsdir2  13574  lgsdirprm  13575  lgsdir  13576  lgsdi  13578  lgsne0  13579  lgsdirnn0  13588  lgsdinn0  13589  2sqlem4  13594  2sqlem9  13600  nnsf  13885  nninfsellemsuc  13892  trilpolemclim  13915  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  trirec0  13923  apdifflemf  13925  apdifflemr  13926  apdiff  13927  iswomni0  13930  nconstwlpolemgt0  13942  nconstwlpolem  13943  neapmkvlem  13945