Theorem mpjaodan 793

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

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

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 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjao3dan  1302  dcun  3525  ifcldadc  3555  ifeq1dadc  3556  ifbothdadc  3557  ifcldcd  3561  exmidn0m  4187  exmidsssn  4188  exmidundif  4192  exmidundifim  4193  ordtri2or2exmidlem  4510  reg2exmidlema  4518  nnpredcl  4607  frecabcl  6378  nnsucuniel  6474  dcdifsnid  6483  phpm  6843  fidifsnen  6848  dif1enen  6858  fin0  6863  fimax2gtrilemstep  6878  finexdc  6880  en2eqpr  6885  fientri3  6892  unsnfidcex  6897  unsnfidcel  6898  undifdcss  6900  fiintim  6906  ssfirab  6911  fidcenumlemrks  6930  fidcenumlemr  6932  omp1eomlem  7071  difinfsnlem  7076  difinfsn  7077  ctssdccl  7088  ctssdc  7090  enumct  7092  nnnninf  7102  nnnninfeq  7104  nnnninfeq2  7105  nninfisol  7109  finomni  7116  ismkvnex  7131  nninfwlpoimlemg  7151  exmidfodomrlemeldju  7176  exmidfodomrlemreseldju  7177  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  exmidontriimlem3  7200  mullocprlem  7532  recexprlemloc  7593  suplocsrlem  7770  btwnapz  9342  xnn0dcle  9759  xnn0letri  9760  z2ge  9783  xaddcom  9818  xnegdi  9825  xaddass  9826  xpncan  9828  xleadd1a  9830  xsubge0  9838  xlesubadd  9840  fztri3or  9995  fzm1  10056  fzneuz  10057  exfzdc  10196  exbtwnzlemstep  10204  rebtwn2zlemstep  10209  apbtwnz  10230  modifeq2int  10342  modsumfzodifsn  10352  iseqf1olemab  10445  iseqf1olemmo  10448  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3f1olemstep  10457  fser0const  10472  expaddzaplem  10519  qsqeqor  10586  expnbnd  10599  nn0ltexp2  10644  apexp1  10652  bcval  10683  bccmpl  10688  bcval5  10697  bcpasc  10700  bccl  10701  hashennnuni  10713  hashnncl  10730  fiubm  10763  zfz1isolemiso  10774  resqrexlemnm  10982  resqrexlemcvg  10983  resqrexlemoverl  10985  resqrexlemglsq  10986  leabs  11038  nn0abscl  11049  ltabs  11051  abslt  11052  fzomaxdif  11077  maxleim  11169  maxabslemval  11172  zmaxcl  11188  2zsupmax  11189  minmax  11193  2zinfmin  11206  xrmaxleim  11207  xrmaxifle  11209  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxiflemcom  11212  xrmaxiflemval  11213  xrmaxaddlem  11223  xrmaxadd  11224  xrminmax  11228  sumdc  11321  sumrbdc  11342  summodclem3  11343  summodclem2a  11344  zsumdc  11347  isumss  11354  fisumss  11355  isumss2  11356  fsumcllem  11362  fsumadd  11369  fsumsplit  11370  fsumsplitsn  11373  sumsplitdc  11395  fisumrev2  11409  fsummulc2  11411  telfsumo  11429  fsumparts  11433  cvgratnnlemseq  11489  cvgratz  11495  fproddccvg  11535  prodrbdc  11537  zproddc  11542  prod1dc  11549  fprodssdc  11553  fprodmul  11554  fprodsplitdc  11559  fprodsplit  11560  fprodunsn  11567  fprodcllem  11569  dvdsle  11804  mod2eq1n2dvds  11838  zsupcllemstep  11900  infssuzex  11904  gcdsupex  11912  gcdsupcl  11913  gcdval  11914  gcddvds  11918  gcdcl  11921  gcd0id  11934  gcdneg  11937  bezoutlemmain  11953  bezoutlemzz  11957  bezoutlemaz  11958  bezoutlembz  11959  dfgcd3  11965  dfgcd2  11969  nn0seqcvgd  11995  eucalgf  12009  eucalginv  12010  dvdslcm  12023  lcmcl  12026  lcmneg  12028  lcmgcd  12032  lcmdvds  12033  lcmid  12034  mulgcddvds  12048  isprm5lem  12095  pw2dvdslemn  12119  sqrt2irrap  12134  phibndlem  12170  prm23ge5  12218  pclemdc  12242  pcge0  12266  pcdvdsb  12273  pceq0  12275  pcneg  12278  pcdvdstr  12280  pcgcd1  12281  pcgcd  12282  pc2dvds  12283  pcz  12285  pcprmpw2  12286  pcaddlem  12292  pcadd  12293  pcmpt  12295  pcmpt2  12296  pcprod  12298  fldivp1  12300  qexpz  12304  1arithlem4  12318  1arith  12319  ennnfonelemss  12365  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ctiunctlemudc  12392  xblss2ps  13198  xblss2  13199  qtopbas  13316  dedekindeulemeu  13394  dedekindeu  13395  suplociccreex  13396  dedekindicclemeu  13403  dedekindicclemicc  13404  limcimolemlt  13427  cnplimclemle  13431  reeff1o  13488  efltlemlt  13489  sin0pilem2  13497  coseq0negpitopi  13551  abssinper  13561  cos02pilt1  13566  logbgcd1irraplemexp  13680  lgslem4  13698  lgsneg  13719  lgsneg1  13720  lgsmod  13721  lgsdilem  13722  lgsdir2  13728  lgsdirprm  13729  lgsdir  13730  lgsdi  13732  lgsne0  13733  lgsdirnn0  13742  lgsdinn0  13743  2sqlem4  13748  2sqlem9  13754  nnsf  14038  nninfsellemsuc  14045  trilpolemclim  14068  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  trirec0  14076  apdifflemf  14078  apdifflemr  14079  apdiff  14080  iswomni0  14083  nconstwlpolemgt0  14095  nconstwlpolem  14096  neapmkvlem  14098