Theorem rexlimddv 3172

Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
rexlimddv.1	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
rexlimddv.2	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)

Assertion

Ref	Expression
rexlimddv	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimddv

Step	Hyp	Ref	Expression
1		rexlimddv.1	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
2		rexlimddv.2	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
3	2	rexlimdvaa 3167	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 16	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is used by:  frxp2  8136  frxp3  8143  oaabs2  8631  oemapvali  9649  cantnflem4  9657  r1pwss  9752  djuun  9917  infxpenc2lem1  10008  pwfseqlem3  10649  prlem934  11022  ltexprlem7  11031  reclem3pr  11038  00id  11389  mul02lem1  11390  addlid  11397  addcan  11398  addcan2  11399  negeu  11451  mulcand  11851  suprzcl  12680  uzwo3  12971  expmulnbnd  14276  limsupgre  15537  rlimclim1  15601  fsumcvg3  15785  oexpneg  16407  bitsfi  16499  vdwlem10  17054  mreexexlem4d  17707  mreexdomd  17709  isacs3lem  18602  grpinvalem  18735  grprida  18737  grprcan  19044  sylow1  19677  pgpfi  19679  slwhash  19698  pj1id  19773  efgsfo  19813  efgredlemc  19819  dmdprdsplitlem  20113  dpjidcl  20134  pgpfac1lem4  20154  pgpfaclem2  20158  pgpfaclem3  20159  ablsimpgcygd  20182  ablsimpgfindlem1  20183  ablsimpgfind  20186  fincygsubgodexd  20189  ablsimpgprmd  20191  gsummgp0  20404  imadrhmcl  20909  lspsolv  21276  restbas  23324  restcls  23347  restntr  23348  cnpnei  23430  cnpco  23433  pnrmopn  23509  1stcfb  23611  1stcrest  23619  2ndcctbss  23621  2ndcomap  23624  dis2ndc  23626  llyidm  23654  nllyidm  23655  hausllycmp  23660  lly1stc  23662  llycmpkgen2  23716  1stckgenlem  23719  basqtop  23877  regr1lem  23905  kqreglem1  23907  kqreglem2  23908  kqnrmlem1  23909  kqnrmlem2  23910  reghmph  23959  nrmhmph  23960  qtophmeo  23983  trfbas2  24009  fbasfip  24034  fbasrn  24050  trfg  24057  ssufl  24084  fmufil  24125  ufldom  24128  uffclsflim  24197  cnpfcfi  24206  alexsublem  24210  alexsubALTlem4  24216  ptcmplem3  24220  ptcmplem4  24221  tsmsxp  24321  met1stc  24687  met2ndci  24688  prdsxmslem2  24695  metcnpi3  24712  icccmplem1  24989  xrge0tsms  25001  metdseq0  25021  cnllycmp  25124  bndth  25126  lebnumlem1  25129  lebnum  25132  cfilfcls  25442  lmle  25469  relcmpcmet  25486  pjthlem2  25606  ovolscalem2  25682  ovolicc2lem4  25688  ovolicc2lem5  25689  ioombl1  25730  uniioombllem6  25756  uniioombl  25757  opnmbllem  25769  volivth  25775  mbfinf  25833  mbfi1fseqlem6  25888  itg2cnlem1  25929  itg2cn  25931  lhop2  26183  dvcnvre  26187  aareccl  26498  aaliou3lem8  26517  aaliou3lem9  26522  ulmdvlem3  26574  mtestbdd  26577  iblulm  26579  radcnvlem1  26585  abelthlem5  26607  abelthlem8  26611  chordthm  27011  dcubic  27020  lgambdd  27210  lgamucov  27211  lgamcvglem  27213  lgamcvg2  27228  fta  27253  dchrptlem2  27438  sumdchr2  27443  2sqlem11  27602  dchrisum  27665  dchrisum0flb  27683  pntibndlem3  27765  pntlemi  27777  cutbdaybnd  27997  cofslts  28120  coinitslts  28121  addsproplem6  28176  negsproplem6  28235  mulsproplem13  28330  mulsproplem14  28331  recsne0  28394  recsex  28421  noseqp1  28493  pjspansn  31938  chscllem3  32000  xmulcand  33249  xrge0tsmsd  33402  esumpcvgval  34477  noinfepfnregs  35553  cnpconn  35730  pconnconn  35731  connpconn  35735  pconnpi1  35737  cnllysconn  35745  cvmcov2  35775  cvmliftpht  35818  mthmpps  36082  sinccvg  36173  btwnconn1lem13  36599  neibastop2lem  36899  tailfb  36916  weiunfr  37006  unblimceq0lem  37123  knoppndvlem9  37137  knoppndvlem21  37149  knoppndvlem22  37150  matunitlindflem2  38296  poimirlem29  38328  opnmbllem0  38335  mblfinlem2  38337  mblfinlem4  38339  prdsbnd2  38474  cntotbnd  38475  heiborlem8  38497  heiborlem9  38498  cvlcvr1  40141  llnmlplnN  40341  cdlemb  40596  paddasslem10  40631  trlcnv  40967  trlator0  40973  trlid0  40978  trlnidatb  40979  cdlemd4  41003  cdlemg5  41407  trlco  41529  cdlemj3  41625  tendo0mul  41628  tendo0mulr  41629  tendoconid  41631  erngdv  41795  erngdv-rN  41803  dihmeetlem1N  42092  dihatlat  42136  hgmaprnlem5N  42702  aks6d1c5  42934  remulcan2d  43052  renegeulemv  43157  remul02  43194  remul01  43196  sn-addcand  43209  sn-addrid  43210  sn-addcan2d  43211  sn-subeu  43216  remulinvcom  43222  remullid  43223  remulcand  43228  rediveud  43232  sn-0tie0  43253  imacrhmcl  43316  fiabv  43332  prjspertr  43365  0prjspnrel  43387  acongrep  43735  jm2.27b  43761  lmhmfgsplit  43841  hbt  43885  imo72b2lem1  44923  mnuss2d  45002  mnuprdlem4  45013  mnuunid  45015  mnurndlem2  45020  cncmpmax  45780  rexlimddv2  46565  stoweidlem62  46804  salrestss  47103  oexpnegALTV  48470  oexpnegnz  48471  upciclem4  49975  aacllem  50649