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  sn0disj  4127  exmidn0m  4340  exmidsssn  4341  exmidundif  4345  exmidundifim  4346  ordtri2or2exmidlem  4675  reg2exmidlema  4683  nnpredcl  4772  frecabcl  6674  nnsucuniel  6772  dcdifsnid  6781  pw2f1odclem  7138  phpm  7171  fidifsnen  7176  dif1enen  7188  fin0  7193  fimax2gtrilemstep  7209  finexdc  7211  elssdc  7213  eqsndc  7214  en2eqpr  7218  fientri3  7226  unsnfidcex  7231  unsnfidcel  7232  undifdcss  7234  prfidceq  7239  tpfidceq  7241  fiintim  7242  ssfirab  7248  fidcenumlemrks  7275  fidcenumlemr  7277  2omap  7324  omp1eomlem  7440  difinfsnlem  7445  difinfsn  7446  ctssdccl  7457  ctssdc  7459  enumct  7461  nninfninc  7469  nnnninf  7472  nnnninfeq  7474  nnnninfeq2  7475  nninfisol  7479  finomni  7486  ismkvnex  7501  nninfwlpoimlemg  7521  pr2cv1  7547  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  exmidontriimlem3  7585  netap  7626  2omotaplemap  7629  mullocprlem  7943  recexprlemloc  8004  suplocsrlem  8181  btwnapz  9787  xnn0dcle  10221  xnn0letri  10222  z2ge  10245  xaddcom  10280  xnegdi  10287  xaddass  10288  xpncan  10290  xleadd1a  10292  xsubge0  10300  xlesubadd  10302  fztri3or  10460  fzm1  10524  fzneuz  10525  exfzdc  10676  zsupcllemstep  10679  infssuzex  10683  exbtwnzlemstep  10699  rebtwn2zlemstep  10704  xqltnle  10719  apbtwnz  10726  flaplt  10739  modifeq2int  10844  modsumfzodifsn  10854  iseqf1olemab  10960  iseqf1olemmo  10963  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  seq3f1olemstep  10972  seqf1oglem1  10977  seqf1oglem2  10978  fser0const  10993  expaddzaplem  11040  qsqeqor  11108  resq01  11116  expnbnd  11122  nn0ltexp2  11169  apexp1  11178  bcval  11209  bccmpl  11214  bcval5  11223  bcpasc  11226  bccl  11227  hashennnuni  11240  hashnncl  11256  fiubm  11293  hashfibc  11305  hashf1  11309  zfz1isolemiso  11313  lswex  11378  ccatsymb  11392  ccat1st1st  11431  fzowrddc  11441  swrd0g  11454  swrdsbslen  11460  swrdspsleq  11461  pfxclz  11473  pfxwrdsymbg  11484  swrdccatin1  11519  resqrexlemnm  11806  resqrexlemcvg  11807  resqrexlemoverl  11809  resqrexlemglsq  11810  leabs  11862  qabscl  11865  nn0abscl  11874  ltabs  11876  abslt  11877  fzomaxdif  11902  maxleim  11994  maxabslemval  11997  zmaxcl  12013  2zsupmax  12015  minmax  12020  zmincl  12029  2zinfmin  12034  xrmaxleim  12035  xrmaxifle  12037  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxiflemcom  12040  xrmaxiflemval  12041  xrmaxaddlem  12051  xrmaxadd  12052  xrminmax  12056  sumdc  12149  fzf1o  12167  sumrbdc  12171  summodclem3  12172  summodclem2a  12173  zsumdc  12176  isumss  12183  fisumss  12184  isumss2  12185  fsumcllem  12191  fsumadd  12198  fsumsplit  12199  fsumsplitsn  12202  sumsplitdc  12224  fisumrev2  12238  fsummulc2  12240  telfsumo  12258  fsumparts  12262  cvgratnnlemseq  12318  cvgratz  12324  fproddccvg  12364  prodrbdc  12366  zproddc  12371  prod1dc  12378  fprodssdc  12382  fprodmul  12383  fprodsplitdc  12388  fprodsplit  12389  fprodunsn  12396  fprodcllem  12398  sinltxirr  12553  fsumdvds  12634  dvdsle  12636  mod2eq1n2dvds  12671  bitsmod  12748  gcdsupex  12759  gcdsupcl  12760  gcdval  12761  gcddvds  12765  gcdcl  12768  gcd0id  12781  gcdneg  12784  bezoutlemmain  12800  bezoutlemzz  12804  bezoutlemaz  12805  bezoutlembz  12806  dfgcd3  12812  dfgcd2  12816  nninfctlemfo  12842  nn0seqcvgd  12844  eucalgf  12858  eucalginv  12859  dvdslcm  12872  lcmcl  12875  lcmneg  12877  lcmgcd  12881  lcmdvds  12882  lcmid  12883  mulgcddvds  12897  prmdcz  12934  isprm5lem  12945  pwbdvdslemn  12969  sqrt2irrap  12985  sqrtrirr  13014  phibndlem  13023  prm23ge5  13072  pclemdc  13096  pcxqcl  13120  pcge0  13121  pcdvdsb  13128  pceq0  13130  pcneg  13133  pcdvdstr  13135  pcgcd1  13136  pcgcd  13137  pc2dvds  13138  pcz  13140  pcprmpw2  13141  pcaddlem  13147  pcadd  13148  pcmpt  13151  pcmpt2  13152  pcprod  13154  fldivp1  13156  qexpz  13160  1arithlem4  13174  1arith  13175  4sqlem19  13217  ennnfonelemss  13359  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ctiunctlemudc  13386  bassetsnn  13467  fvprif  13723  gzsumwsubmcl  13860  gzsumwmhm  13862  gzsumcl  13863  mulgnn0p1  13995  mulgnn0subcl  13997  mulgsubcl  13998  mulgneg  14002  mulgz  14012  mulgnn0dir  14014  mulgdirlem  14015  mulgdir  14016  submmulg  14028  ghmmulg  14118  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  gzsumsplit0  14238  gsumvalfi  14242  gzsumgsum  14245  gsummptfidmsplit  14254  gsumresfi  14263  gsum2d2fi  14274  lringuplu  14612  aprlring  14709  znf1o  15095  xblss2ps  15630  xblss2  15631  qtopbas  15748  dedekindeulemeu  15848  dedekindeu  15849  suplociccreex  15850  dedekindicclemeu  15857  dedekindicclemicc  15858  limcimolemlt  15890  cnplimclemle  15894  dvmptc  15943  reeff1o  15999  efltlemlt  16000  efap1p  16005  sin0pilem2  16009  coseq0negpitopi  16063  abssinper  16073  cos02pilt1  16079  logdivlt  16124  logbgcd1irraplemexp  16204  birthdaylem2  16226  birthdaylem3  16227  ppiqp1le  16267  ppiqltx  16281  ppiqub  16293  chtqub  16296  bcmono  16304  bcmax  16305  bposlem3  16313  bposlem5  16315  bposlem6  16316  bpos  16320  lgslem4  16327  lgsneg  16348  lgsneg1  16349  lgsmod  16350  lgsdilem  16351  lgsdir2  16357  lgsdirprm  16358  lgsdir  16359  lgsdi  16361  lgsne0  16362  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  gausslemma2dlem4  16388  lgseisenlem1  16394  lgsquad3  16408  2sqlem4  16442  2sqlem9  16448  eupth2lem3lem3fi  16916  eupth2lem3lem4fi  16919  eupth2lem3lem7fi  16920  dichmul0orlem3  16960  dichmul0orlem7  16964  nnsf  17254  nninfsellemsuc  17261  nnnninfex  17271  trilpolemclim  17292  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  trirec0  17300  apdifflemf  17302  apdifflemr  17303  apdiff  17304  iswomni0  17308  nconstwlpolemgt0  17321  nconstwlpolem  17322  neapmkvlem  17324