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  3560  ifcldadc  3590  ifeq1dadc  3591  ifeq2dadc  3592  ifbothdadc  3593  ifcldcd  3597  exmidn0m  4234  exmidsssn  4235  exmidundif  4239  exmidundifim  4240  ordtri2or2exmidlem  4562  reg2exmidlema  4570  nnpredcl  4659  frecabcl  6457  nnsucuniel  6553  dcdifsnid  6562  pw2f1odclem  6895  phpm  6926  fidifsnen  6931  dif1enen  6941  fin0  6946  fimax2gtrilemstep  6961  finexdc  6963  en2eqpr  6968  fientri3  6976  unsnfidcex  6981  unsnfidcel  6982  undifdcss  6984  prfidceq  6989  tpfidceq  6991  fiintim  6992  ssfirab  6997  fidcenumlemrks  7019  fidcenumlemr  7021  omp1eomlem  7160  difinfsnlem  7165  difinfsn  7166  ctssdccl  7177  ctssdc  7179  enumct  7181  nninfninc  7189  nnnninf  7192  nnnninfeq  7194  nnnninfeq2  7195  nninfisol  7199  finomni  7206  ismkvnex  7221  nninfwlpoimlemg  7241  exmidfodomrlemeldju  7266  exmidfodomrlemreseldju  7267  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  exmidontriimlem3  7290  netap  7321  2omotaplemap  7324  mullocprlem  7637  recexprlemloc  7698  suplocsrlem  7875  btwnapz  9456  xnn0dcle  9877  xnn0letri  9878  z2ge  9901  xaddcom  9936  xnegdi  9943  xaddass  9944  xpncan  9946  xleadd1a  9948  xsubge0  9956  xlesubadd  9958  fztri3or  10114  fzm1  10175  fzneuz  10176  exfzdc  10316  zsupcllemstep  10319  infssuzex  10323  exbtwnzlemstep  10337  rebtwn2zlemstep  10342  xqltnle  10357  apbtwnz  10364  modifeq2int  10478  modsumfzodifsn  10488  iseqf1olemab  10594  iseqf1olemmo  10597  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seq3f1olemstep  10606  seqf1oglem1  10611  seqf1oglem2  10612  fser0const  10627  expaddzaplem  10674  qsqeqor  10742  expnbnd  10755  nn0ltexp2  10801  apexp1  10810  bcval  10841  bccmpl  10846  bcval5  10855  bcpasc  10858  bccl  10859  hashennnuni  10871  hashnncl  10887  fiubm  10920  zfz1isolemiso  10931  resqrexlemnm  11183  resqrexlemcvg  11184  resqrexlemoverl  11186  resqrexlemglsq  11187  leabs  11239  nn0abscl  11250  ltabs  11252  abslt  11253  fzomaxdif  11278  maxleim  11370  maxabslemval  11373  zmaxcl  11389  2zsupmax  11391  minmax  11395  2zinfmin  11408  xrmaxleim  11409  xrmaxifle  11411  xrmaxiflemab  11412  xrmaxiflemlub  11413  xrmaxiflemcom  11414  xrmaxiflemval  11415  xrmaxaddlem  11425  xrmaxadd  11426  xrminmax  11430  sumdc  11523  sumrbdc  11544  summodclem3  11545  summodclem2a  11546  zsumdc  11549  isumss  11556  fisumss  11557  isumss2  11558  fsumcllem  11564  fsumadd  11571  fsumsplit  11572  fsumsplitsn  11575  sumsplitdc  11597  fisumrev2  11611  fsummulc2  11613  telfsumo  11631  fsumparts  11635  cvgratnnlemseq  11691  cvgratz  11697  fproddccvg  11737  prodrbdc  11739  zproddc  11744  prod1dc  11751  fprodssdc  11755  fprodmul  11756  fprodsplitdc  11761  fprodsplit  11762  fprodunsn  11769  fprodcllem  11771  sinltxirr  11926  fsumdvds  12007  dvdsle  12009  mod2eq1n2dvds  12044  gcdsupex  12124  gcdsupcl  12125  gcdval  12126  gcddvds  12130  gcdcl  12133  gcd0id  12146  gcdneg  12149  bezoutlemmain  12165  bezoutlemzz  12169  bezoutlemaz  12170  bezoutlembz  12171  dfgcd3  12177  dfgcd2  12181  nninfctlemfo  12207  nn0seqcvgd  12209  eucalgf  12223  eucalginv  12224  dvdslcm  12237  lcmcl  12240  lcmneg  12242  lcmgcd  12246  lcmdvds  12247  lcmid  12248  mulgcddvds  12262  isprm5lem  12309  pw2dvdslemn  12333  sqrt2irrap  12348  phibndlem  12384  prm23ge5  12433  pclemdc  12457  pcxqcl  12481  pcge0  12482  pcdvdsb  12489  pceq0  12491  pcneg  12494  pcdvdstr  12496  pcgcd1  12497  pcgcd  12498  pc2dvds  12499  pcz  12501  pcprmpw2  12502  pcaddlem  12508  pcadd  12509  pcmpt  12512  pcmpt2  12513  pcprod  12515  fldivp1  12517  qexpz  12521  1arithlem4  12535  1arith  12536  4sqlem19  12578  ennnfonelemss  12627  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ctiunctlemudc  12654  fvprif  12986  gsumfzz  13127  gsumwsubmcl  13128  gsumwmhm  13130  gsumfzcl  13131  mulgnn0p1  13263  mulgnn0subcl  13265  mulgsubcl  13266  mulgneg  13270  mulgz  13280  mulgnn0dir  13282  mulgdirlem  13283  mulgdir  13284  submmulg  13296  ghmmulg  13386  gsumfzreidx  13467  gsumfzsubmcl  13468  gsumfzmptfidmadd  13469  gsumfzmhm  13473  lringuplu  13752  gsumfzfsum  14144  znf1o  14207  xblss2ps  14640  xblss2  14641  qtopbas  14758  dedekindeulemeu  14858  dedekindeu  14859  suplociccreex  14860  dedekindicclemeu  14867  dedekindicclemicc  14868  limcimolemlt  14900  cnplimclemle  14904  dvmptc  14953  reeff1o  15009  efltlemlt  15010  sin0pilem2  15018  coseq0negpitopi  15072  abssinper  15082  cos02pilt1  15087  logbgcd1irraplemexp  15204  lgslem4  15244  lgsneg  15265  lgsneg1  15266  lgsmod  15267  lgsdilem  15268  lgsdir2  15274  lgsdirprm  15275  lgsdir  15276  lgsdi  15278  lgsne0  15279  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem4  15305  lgseisenlem1  15311  lgsquad3  15325  2sqlem4  15359  2sqlem9  15365  nnsf  15649  nninfsellemsuc  15656  trilpolemclim  15680  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  trirec0  15688  apdifflemf  15690  apdifflemr  15691  apdiff  15692  iswomni0  15695  nconstwlpolemgt0  15708  nconstwlpolem  15709  neapmkvlem  15711