Theorem mpjaodan 799

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

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1318  dcun  3561  ifcldadc  3591  ifeq1dadc  3592  ifeq2dadc  3593  ifbothdadc  3594  ifcldcd  3598  exmidn0m  4235  exmidsssn  4236  exmidundif  4240  exmidundifim  4241  ordtri2or2exmidlem  4563  reg2exmidlema  4571  nnpredcl  4660  frecabcl  6466  nnsucuniel  6562  dcdifsnid  6571  pw2f1odclem  6904  phpm  6935  fidifsnen  6940  dif1enen  6950  fin0  6955  fimax2gtrilemstep  6970  finexdc  6972  en2eqpr  6977  fientri3  6985  unsnfidcex  6990  unsnfidcel  6991  undifdcss  6993  prfidceq  6998  tpfidceq  7000  fiintim  7001  ssfirab  7006  fidcenumlemrks  7028  fidcenumlemr  7030  omp1eomlem  7169  difinfsnlem  7174  difinfsn  7175  ctssdccl  7186  ctssdc  7188  enumct  7190  nninfninc  7198  nnnninf  7201  nnnninfeq  7203  nnnninfeq2  7204  nninfisol  7208  finomni  7215  ismkvnex  7230  nninfwlpoimlemg  7250  exmidfodomrlemeldju  7280  exmidfodomrlemreseldju  7281  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidaclem  7293  exmidontriimlem3  7308  netap  7339  2omotaplemap  7342  mullocprlem  7656  recexprlemloc  7717  suplocsrlem  7894  btwnapz  9475  xnn0dcle  9896  xnn0letri  9897  z2ge  9920  xaddcom  9955  xnegdi  9962  xaddass  9963  xpncan  9965  xleadd1a  9967  xsubge0  9975  xlesubadd  9977  fztri3or  10133  fzm1  10194  fzneuz  10195  exfzdc  10335  zsupcllemstep  10338  infssuzex  10342  exbtwnzlemstep  10356  rebtwn2zlemstep  10361  xqltnle  10376  apbtwnz  10383  modifeq2int  10497  modsumfzodifsn  10507  iseqf1olemab  10613  iseqf1olemmo  10616  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seq3f1olemstep  10625  seqf1oglem1  10630  seqf1oglem2  10631  fser0const  10646  expaddzaplem  10693  qsqeqor  10761  expnbnd  10774  nn0ltexp2  10820  apexp1  10829  bcval  10860  bccmpl  10865  bcval5  10874  bcpasc  10877  bccl  10878  hashennnuni  10890  hashnncl  10906  fiubm  10939  zfz1isolemiso  10950  resqrexlemnm  11202  resqrexlemcvg  11203  resqrexlemoverl  11205  resqrexlemglsq  11206  leabs  11258  nn0abscl  11269  ltabs  11271  abslt  11272  fzomaxdif  11297  maxleim  11389  maxabslemval  11392  zmaxcl  11408  2zsupmax  11410  minmax  11414  2zinfmin  11427  xrmaxleim  11428  xrmaxifle  11430  xrmaxiflemab  11431  xrmaxiflemlub  11432  xrmaxiflemcom  11433  xrmaxiflemval  11434  xrmaxaddlem  11444  xrmaxadd  11445  xrminmax  11449  sumdc  11542  sumrbdc  11563  summodclem3  11564  summodclem2a  11565  zsumdc  11568  isumss  11575  fisumss  11576  isumss2  11577  fsumcllem  11583  fsumadd  11590  fsumsplit  11591  fsumsplitsn  11594  sumsplitdc  11616  fisumrev2  11630  fsummulc2  11632  telfsumo  11650  fsumparts  11654  cvgratnnlemseq  11710  cvgratz  11716  fproddccvg  11756  prodrbdc  11758  zproddc  11763  prod1dc  11770  fprodssdc  11774  fprodmul  11775  fprodsplitdc  11780  fprodsplit  11781  fprodunsn  11788  fprodcllem  11790  sinltxirr  11945  fsumdvds  12026  dvdsle  12028  mod2eq1n2dvds  12063  bitsmod  12140  gcdsupex  12151  gcdsupcl  12152  gcdval  12153  gcddvds  12157  gcdcl  12160  gcd0id  12173  gcdneg  12176  bezoutlemmain  12192  bezoutlemzz  12196  bezoutlemaz  12197  bezoutlembz  12198  dfgcd3  12204  dfgcd2  12208  nninfctlemfo  12234  nn0seqcvgd  12236  eucalgf  12250  eucalginv  12251  dvdslcm  12264  lcmcl  12267  lcmneg  12269  lcmgcd  12273  lcmdvds  12274  lcmid  12275  mulgcddvds  12289  isprm5lem  12336  pw2dvdslemn  12360  sqrt2irrap  12375  phibndlem  12411  prm23ge5  12460  pclemdc  12484  pcxqcl  12508  pcge0  12509  pcdvdsb  12516  pceq0  12518  pcneg  12521  pcdvdstr  12523  pcgcd1  12524  pcgcd  12525  pc2dvds  12526  pcz  12528  pcprmpw2  12529  pcaddlem  12535  pcadd  12536  pcmpt  12539  pcmpt2  12540  pcprod  12542  fldivp1  12544  qexpz  12548  1arithlem4  12562  1arith  12563  4sqlem19  12605  ennnfonelemss  12654  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ctiunctlemudc  12681  fvprif  13047  gsumfzz  13199  gsumwsubmcl  13200  gsumwmhm  13202  gsumfzcl  13203  mulgnn0p1  13341  mulgnn0subcl  13343  mulgsubcl  13344  mulgneg  13348  mulgz  13358  mulgnn0dir  13360  mulgdirlem  13361  mulgdir  13362  submmulg  13374  ghmmulg  13464  gsumfzreidx  13545  gsumfzsubmcl  13546  gsumfzmptfidmadd  13547  gsumfzmhm  13551  lringuplu  13830  gsumfzfsum  14222  znf1o  14285  xblss2ps  14748  xblss2  14749  qtopbas  14866  dedekindeulemeu  14966  dedekindeu  14967  suplociccreex  14968  dedekindicclemeu  14975  dedekindicclemicc  14976  limcimolemlt  15008  cnplimclemle  15012  dvmptc  15061  reeff1o  15117  efltlemlt  15118  sin0pilem2  15126  coseq0negpitopi  15180  abssinper  15190  cos02pilt1  15195  logbgcd1irraplemexp  15312  lgslem4  15352  lgsneg  15373  lgsneg1  15374  lgsmod  15375  lgsdilem  15376  lgsdir2  15382  lgsdirprm  15383  lgsdir  15384  lgsdi  15386  lgsne0  15387  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  gausslemma2dlem4  15413  lgseisenlem1  15419  lgsquad3  15433  2sqlem4  15467  2sqlem9  15473  2omap  15750  nnsf  15760  nninfsellemsuc  15767  nnnninfex  15777  trilpolemclim  15793  trilpolemisumle  15795  trilpolemeq1  15797  trilpolemlt1  15798  trirec0  15801  apdifflemf  15803  apdifflemr  15804  apdiff  15805  iswomni0  15808  nconstwlpolemgt0  15821  nconstwlpolem  15822  neapmkvlem  15824