Theorem mpjaodan 805

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1343  dcun  3604  ifcldadc  3635  ifeq1dadc  3636  ifeq2dadc  3637  ifeqdadc  3638  ifbothdadc  3639  ifcldcd  3643  2if2dc  3645  exmidn0m  4291  exmidsssn  4292  exmidundif  4296  exmidundifim  4297  ordtri2or2exmidlem  4624  reg2exmidlema  4632  nnpredcl  4721  frecabcl  6564  nnsucuniel  6662  dcdifsnid  6671  pw2f1odclem  7019  phpm  7051  fidifsnen  7056  dif1enen  7068  fin0  7073  fimax2gtrilemstep  7089  finexdc  7091  elssdc  7093  eqsndc  7094  en2eqpr  7098  fientri3  7106  unsnfidcex  7111  unsnfidcel  7112  undifdcss  7114  prfidceq  7119  tpfidceq  7121  fiintim  7122  ssfirab  7128  fidcenumlemrks  7151  fidcenumlemr  7153  omp1eomlem  7292  difinfsnlem  7297  difinfsn  7298  ctssdccl  7309  ctssdc  7311  enumct  7313  nninfninc  7321  nnnninf  7324  nnnninfeq  7326  nnnninfeq2  7327  nninfisol  7331  finomni  7338  ismkvnex  7353  nninfwlpoimlemg  7373  pr2cv1  7399  exmidfodomrlemeldju  7409  exmidfodomrlemreseldju  7410  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidaclem  7422  exmidontriimlem3  7437  netap  7472  2omotaplemap  7475  mullocprlem  7789  recexprlemloc  7850  suplocsrlem  8027  btwnapz  9609  xnn0dcle  10036  xnn0letri  10037  z2ge  10060  xaddcom  10095  xnegdi  10102  xaddass  10103  xpncan  10105  xleadd1a  10107  xsubge0  10115  xlesubadd  10117  fztri3or  10273  fzm1  10334  fzneuz  10335  exfzdc  10485  zsupcllemstep  10488  infssuzex  10492  exbtwnzlemstep  10506  rebtwn2zlemstep  10511  xqltnle  10526  apbtwnz  10533  modifeq2int  10647  modsumfzodifsn  10657  iseqf1olemab  10763  iseqf1olemmo  10766  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seq3f1olemstep  10775  seqf1oglem1  10780  seqf1oglem2  10781  fser0const  10796  expaddzaplem  10843  qsqeqor  10911  expnbnd  10924  nn0ltexp2  10970  apexp1  10979  bcval  11010  bccmpl  11015  bcval5  11024  bcpasc  11027  bccl  11028  hashennnuni  11040  hashnncl  11056  fiubm  11091  zfz1isolemiso  11102  lswex  11164  ccatsymb  11178  ccat1st1st  11217  fzowrddc  11227  swrd0g  11240  swrdsbslen  11246  swrdspsleq  11247  pfxclz  11259  pfxwrdsymbg  11270  swrdccatin1  11305  resqrexlemnm  11578  resqrexlemcvg  11579  resqrexlemoverl  11581  resqrexlemglsq  11582  leabs  11634  nn0abscl  11645  ltabs  11647  abslt  11648  fzomaxdif  11673  maxleim  11765  maxabslemval  11768  zmaxcl  11784  2zsupmax  11786  minmax  11790  2zinfmin  11803  xrmaxleim  11804  xrmaxifle  11806  xrmaxiflemab  11807  xrmaxiflemlub  11808  xrmaxiflemcom  11809  xrmaxiflemval  11810  xrmaxaddlem  11820  xrmaxadd  11821  xrminmax  11825  sumdc  11918  sumrbdc  11939  summodclem3  11940  summodclem2a  11941  zsumdc  11944  isumss  11951  fisumss  11952  isumss2  11953  fsumcllem  11959  fsumadd  11966  fsumsplit  11967  fsumsplitsn  11970  sumsplitdc  11992  fisumrev2  12006  fsummulc2  12008  telfsumo  12026  fsumparts  12030  cvgratnnlemseq  12086  cvgratz  12092  fproddccvg  12132  prodrbdc  12134  zproddc  12139  prod1dc  12146  fprodssdc  12150  fprodmul  12151  fprodsplitdc  12156  fprodsplit  12157  fprodunsn  12164  fprodcllem  12166  sinltxirr  12321  fsumdvds  12402  dvdsle  12404  mod2eq1n2dvds  12439  bitsmod  12516  gcdsupex  12527  gcdsupcl  12528  gcdval  12529  gcddvds  12533  gcdcl  12536  gcd0id  12549  gcdneg  12552  bezoutlemmain  12568  bezoutlemzz  12572  bezoutlemaz  12573  bezoutlembz  12574  dfgcd3  12580  dfgcd2  12584  nninfctlemfo  12610  nn0seqcvgd  12612  eucalgf  12626  eucalginv  12627  dvdslcm  12640  lcmcl  12643  lcmneg  12645  lcmgcd  12649  lcmdvds  12650  lcmid  12651  mulgcddvds  12665  isprm5lem  12712  pw2dvdslemn  12736  sqrt2irrap  12751  phibndlem  12787  prm23ge5  12836  pclemdc  12860  pcxqcl  12884  pcge0  12885  pcdvdsb  12892  pceq0  12894  pcneg  12897  pcdvdstr  12899  pcgcd1  12900  pcgcd  12901  pc2dvds  12902  pcz  12904  pcprmpw2  12905  pcaddlem  12911  pcadd  12912  pcmpt  12915  pcmpt2  12916  pcprod  12918  fldivp1  12920  qexpz  12924  1arithlem4  12938  1arith  12939  4sqlem19  12981  ennnfonelemss  13030  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ctiunctlemudc  13057  bassetsnn  13138  fvprif  13425  gsumfzz  13577  gsumwsubmcl  13578  gsumwmhm  13580  gsumfzcl  13581  mulgnn0p1  13719  mulgnn0subcl  13721  mulgsubcl  13722  mulgneg  13726  mulgz  13736  mulgnn0dir  13738  mulgdirlem  13739  mulgdir  13740  submmulg  13752  ghmmulg  13842  gsumfzreidx  13923  gsumfzsubmcl  13924  gsumfzmptfidmadd  13925  gsumfzmhm  13929  lringuplu  14209  gsumfzfsum  14601  znf1o  14664  xblss2ps  15127  xblss2  15128  qtopbas  15245  dedekindeulemeu  15345  dedekindeu  15346  suplociccreex  15347  dedekindicclemeu  15354  dedekindicclemicc  15355  limcimolemlt  15387  cnplimclemle  15391  dvmptc  15440  reeff1o  15496  efltlemlt  15497  sin0pilem2  15505  coseq0negpitopi  15559  abssinper  15569  cos02pilt1  15574  logbgcd1irraplemexp  15691  lgslem4  15731  lgsneg  15752  lgsneg1  15753  lgsmod  15754  lgsdilem  15755  lgsdir2  15761  lgsdirprm  15762  lgsdir  15763  lgsdi  15765  lgsne0  15766  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem4  15792  lgseisenlem1  15798  lgsquad3  15812  2sqlem4  15846  2sqlem9  15852  2omap  16594  nnsf  16607  nninfsellemsuc  16614  nnnninfex  16624  trilpolemclim  16640  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  trirec0  16648  apdifflemf  16650  apdifflemr  16651  apdiff  16652  iswomni0  16655  nconstwlpolemgt0  16668  nconstwlpolem  16669  neapmkvlem  16671  gfsumval  16680  gsumgfsum  16684