Theorem mpjaodan 810

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjao3dan  1348  dcun  3637  ifcldadc  3670  ifeq1dadc  3671  ifeq2dadc  3672  ifeqdadc  3673  ifbothdadc  3674  ifcldcd  3678  2if2dc  3680  ifeqeqxdc  3687  exmidn0m  4338  exmidsssn  4339  exmidundif  4343  exmidundifim  4344  ordtri2or2exmidlem  4673  reg2exmidlema  4681  nnpredcl  4770  frecabcl  6670  nnsucuniel  6768  dcdifsnid  6777  pw2f1odclem  7134  phpm  7167  fidifsnen  7172  dif1enen  7184  fin0  7189  fimax2gtrilemstep  7205  finexdc  7207  elssdc  7209  eqsndc  7210  en2eqpr  7214  fientri3  7222  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  prfidceq  7235  tpfidceq  7237  fiintim  7238  ssfirab  7244  fidcenumlemrks  7270  fidcenumlemr  7272  2omap  7318  omp1eomlem  7434  difinfsnlem  7439  difinfsn  7440  ctssdccl  7451  ctssdc  7453  enumct  7455  nninfninc  7463  nnnninf  7466  nnnninfeq  7468  nnnninfeq2  7469  nninfisol  7473  finomni  7480  ismkvnex  7495  nninfwlpoimlemg  7515  pr2cv1  7541  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  exmidontriimlem3  7579  netap  7620  2omotaplemap  7623  mullocprlem  7937  recexprlemloc  7998  suplocsrlem  8175  btwnapz  9780  xnn0dcle  10214  xnn0letri  10215  z2ge  10238  xaddcom  10273  xnegdi  10280  xaddass  10281  xpncan  10283  xleadd1a  10285  xsubge0  10293  xlesubadd  10295  fztri3or  10453  fzm1  10517  fzneuz  10518  exfzdc  10669  zsupcllemstep  10672  infssuzex  10676  exbtwnzlemstep  10692  rebtwn2zlemstep  10697  xqltnle  10712  apbtwnz  10719  modifeq2int  10836  modsumfzodifsn  10846  iseqf1olemab  10952  iseqf1olemmo  10955  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  seq3f1olemstep  10964  seqf1oglem1  10969  seqf1oglem2  10970  fser0const  10985  expaddzaplem  11032  qsqeqor  11100  resq01  11108  expnbnd  11114  nn0ltexp2  11161  apexp1  11170  bcval  11201  bccmpl  11206  bcval5  11215  bcpasc  11218  bccl  11219  hashennnuni  11232  hashnncl  11248  fiubm  11285  hashfibc  11297  hashf1  11301  zfz1isolemiso  11305  lswex  11370  ccatsymb  11384  ccat1st1st  11423  fzowrddc  11433  swrd0g  11446  swrdsbslen  11452  swrdspsleq  11453  pfxclz  11465  pfxwrdsymbg  11476  swrdccatin1  11511  resqrexlemnm  11798  resqrexlemcvg  11799  resqrexlemoverl  11801  resqrexlemglsq  11802  leabs  11854  qabscl  11857  nn0abscl  11866  ltabs  11868  abslt  11869  fzomaxdif  11894  maxleim  11986  maxabslemval  11989  zmaxcl  12005  2zsupmax  12007  minmax  12011  zmincl  12020  2zinfmin  12025  xrmaxleim  12026  xrmaxifle  12028  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxiflemcom  12031  xrmaxiflemval  12032  xrmaxaddlem  12042  xrmaxadd  12043  xrminmax  12047  sumdc  12140  fzf1o  12158  sumrbdc  12162  summodclem3  12163  summodclem2a  12164  zsumdc  12167  isumss  12174  fisumss  12175  isumss2  12176  fsumcllem  12182  fsumadd  12189  fsumsplit  12190  fsumsplitsn  12193  sumsplitdc  12215  fisumrev2  12229  fsummulc2  12231  telfsumo  12249  fsumparts  12253  cvgratnnlemseq  12309  cvgratz  12315  fproddccvg  12355  prodrbdc  12357  zproddc  12362  prod1dc  12369  fprodssdc  12373  fprodmul  12374  fprodsplitdc  12379  fprodsplit  12380  fprodunsn  12387  fprodcllem  12389  sinltxirr  12544  fsumdvds  12625  dvdsle  12627  mod2eq1n2dvds  12662  bitsmod  12739  gcdsupex  12750  gcdsupcl  12751  gcdval  12752  gcddvds  12756  gcdcl  12759  gcd0id  12772  gcdneg  12775  bezoutlemmain  12791  bezoutlemzz  12795  bezoutlemaz  12796  bezoutlembz  12797  dfgcd3  12803  dfgcd2  12807  nninfctlemfo  12833  nn0seqcvgd  12835  eucalgf  12849  eucalginv  12850  dvdslcm  12863  lcmcl  12866  lcmneg  12868  lcmgcd  12872  lcmdvds  12873  lcmid  12874  mulgcddvds  12888  prmdcz  12925  isprm5lem  12936  pwbdvdslemn  12960  sqrt2irrap  12976  sqrtrirr  13005  phibndlem  13014  prm23ge5  13063  pclemdc  13087  pcxqcl  13111  pcge0  13112  pcdvdsb  13119  pceq0  13121  pcneg  13124  pcdvdstr  13126  pcgcd1  13127  pcgcd  13128  pc2dvds  13129  pcz  13131  pcprmpw2  13132  pcaddlem  13138  pcadd  13139  pcmpt  13142  pcmpt2  13143  pcprod  13145  fldivp1  13147  qexpz  13151  1arithlem4  13165  1arith  13166  4sqlem19  13208  ennnfonelemss  13350  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ctiunctlemudc  13377  bassetsnn  13458  fvprif  13713  gzsumwsubmcl  13850  gzsumwmhm  13852  gzsumcl  13853  mulgnn0p1  13985  mulgnn0subcl  13987  mulgsubcl  13988  mulgneg  13992  mulgz  14002  mulgnn0dir  14004  mulgdirlem  14005  mulgdir  14006  submmulg  14018  ghmmulg  14108  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  gzsumsplit0  14197  gsumvalfi  14201  gzsumgsum  14204  lringuplu  14552  aprlring  14649  znf1o  15035  xblss2ps  15554  xblss2  15555  qtopbas  15672  dedekindeulemeu  15772  dedekindeu  15773  suplociccreex  15774  dedekindicclemeu  15781  dedekindicclemicc  15782  limcimolemlt  15814  cnplimclemle  15818  dvmptc  15867  reeff1o  15923  efltlemlt  15924  efap1p  15929  sin0pilem2  15933  coseq0negpitopi  15987  abssinper  15997  cos02pilt1  16002  logdivlt  16046  logbgcd1irraplemexp  16123  birthdaylem2  16145  birthdaylem3  16146  ppiqp1le  16173  ppiqltx  16183  ppiqub  16194  bcmono  16202  bcmax  16203  bposlem3  16211  bposlem5  16213  lgslem4  16220  lgsneg  16241  lgsneg1  16242  lgsmod  16243  lgsdilem  16244  lgsdir2  16250  lgsdirprm  16251  lgsdir  16252  lgsdi  16254  lgsne0  16255  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  gausslemma2dlem4  16281  lgseisenlem1  16287  lgsquad3  16301  2sqlem4  16335  2sqlem9  16341  eupth2lem3lem3fi  16809  eupth2lem3lem4fi  16812  eupth2lem3lem7fi  16813  dichmul0orlem3  16853  dichmul0orlem7  16857  nnsf  17146  nninfsellemsuc  17153  nnnninfex  17163  trilpolemclim  17183  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  trirec0  17191  apdifflemf  17193  apdifflemr  17194  apdiff  17195  iswomni0  17199  nconstwlpolemgt0  17212  nconstwlpolem  17213  neapmkvlem  17215