Theorem rexlimddv 3154

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 3149	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3070

This theorem is referenced by:  frxp2  8081  frxp3  8088  oaabs2  8600  oemapvali  9629  cantnflem4  9637  r1pwss  9729  djuun  9871  infxpenc2lem1  9964  pwfseqlem3  10605  prlem934  10978  ltexprlem7  10987  reclem3pr  10994  00id  11339  mul02lem1  11340  addlid  11347  addcan  11348  addcan2  11349  negeu  11400  mulcand  11797  suprzcl  12592  uzwo3  12877  expmulnbnd  14148  limsupgre  15375  rlimclim1  15439  fsumcvg3  15625  oexpneg  16238  bitsfi  16328  vdwlem10  16873  mreexexlem4d  17541  mreexdomd  17543  isacs3lem  18445  grprinvlem  18542  grpridd  18544  grprcan  18798  sylow1  19399  pgpfi  19401  slwhash  19420  pj1id  19495  efgsfo  19535  efgredlemc  19541  dmdprdsplitlem  19830  dpjidcl  19851  pgpfac1lem4  19871  pgpfaclem2  19875  pgpfaclem3  19876  ablsimpgcygd  19899  ablsimpgfindlem1  19900  ablsimpgfind  19903  fincygsubgodexd  19906  ablsimpgprmd  19908  gsummgp0  20046  imadrhmcl  20320  lspsolv  20663  restbas  22546  restcls  22569  restntr  22570  cnpnei  22652  cnpco  22655  pnrmopn  22731  1stcfb  22833  1stcrest  22841  2ndcctbss  22843  2ndcomap  22846  dis2ndc  22848  llyidm  22876  nllyidm  22877  hausllycmp  22882  lly1stc  22884  llycmpkgen2  22938  1stckgenlem  22941  basqtop  23099  regr1lem  23127  kqreglem1  23129  kqreglem2  23130  kqnrmlem1  23131  kqnrmlem2  23132  reghmph  23181  nrmhmph  23182  qtophmeo  23205  trfbas2  23231  fbasfip  23256  fbasrn  23272  trfg  23279  ssufl  23306  fmufil  23347  ufldom  23350  uffclsflim  23419  cnpfcfi  23428  alexsublem  23432  alexsubALTlem4  23438  ptcmplem3  23442  ptcmplem4  23443  tsmsxp  23543  met1stc  23914  met2ndci  23915  prdsxmslem2  23922  metcnpi3  23939  icccmplem1  24222  xrge0tsms  24234  metdseq0  24254  cnllycmp  24356  bndth  24358  lebnumlem1  24361  lebnum  24364  cfilfcls  24675  lmle  24702  relcmpcmet  24719  pjthlem2  24839  ovolscalem2  24915  ovolicc2lem4  24921  ovolicc2lem5  24922  ioombl1  24963  uniioombllem6  24989  uniioombl  24990  opnmbllem  25002  volivth  25008  mbfinf  25066  mbfi1fseqlem6  25122  itg2cnlem1  25163  itg2cn  25165  lhop2  25416  dvcnvre  25420  aareccl  25723  aaliou3lem8  25742  aaliou3lem9  25747  ulmdvlem3  25798  mtestbdd  25801  iblulm  25803  radcnvlem1  25809  abelthlem5  25831  abelthlem8  25835  chordthm  26224  dcubic  26233  lgambdd  26423  lgamucov  26424  lgamcvglem  26426  lgamcvg2  26441  fta  26466  dchrptlem2  26650  sumdchr2  26655  2sqlem11  26814  dchrisum  26877  dchrisum0flb  26895  pntibndlem3  26977  pntlemi  26989  scutbdaybnd  27197  cofsslt  27280  coinitsslt  27281  addsproplem6  27329  negsproplem6  27374  pjspansn  30582  chscllem3  30644  xmulcand  31847  xrge0tsmsd  31969  esumpcvgval  32766  cnpconn  33911  pconnconn  33912  connpconn  33916  pconnpi1  33918  cnllysconn  33926  cvmcov2  33956  cvmliftpht  33999  mthmpps  34263  sinccvg  34348  btwnconn1lem13  34760  neibastop2lem  34908  tailfb  34925  unblimceq0lem  35045  knoppndvlem9  35059  knoppndvlem21  35071  knoppndvlem22  35072  matunitlindflem2  36148  poimirlem29  36180  opnmbllem0  36187  mblfinlem2  36189  mblfinlem4  36191  prdsbnd2  36327  cntotbnd  36328  heiborlem8  36350  heiborlem9  36351  cvlcvr1  37874  llnmlplnN  38075  cdlemb  38330  paddasslem10  38365  trlcnv  38701  trlator0  38707  trlid0  38712  trlnidatb  38713  cdlemd4  38737  cdlemg5  39141  trlco  39263  cdlemj3  39359  tendo0mul  39362  tendo0mulr  39363  tendoconid  39365  erngdv  39529  erngdv-rN  39537  dihmeetlem1N  39826  dihatlat  39870  hgmaprnlem5N  40436  imacrhmcl  40762  remulcan2d  40837  renegeulemv  40895  remul02  40932  remul01  40934  sn-addcand  40946  sn-addrid  40947  sn-addcan2d  40948  sn-subeu  40953  remulinvcom  40959  remullid  40960  remulcand  40965  sn-0tie0  40966  itrere  40993  retire  40994  prjspertr  41001  0prjspnrel  41023  acongrep  41362  jm2.27b  41388  lmhmfgsplit  41471  hbt  41515  imo72b2lem1  42564  mnuss2d  42666  mnuprdlem4  42677  mnuunid  42679  mnurndlem2  42684  cncmpmax  43359  rexlimddv2  44184  stoweidlem62  44423  salrestss  44722  oexpnegALTV  45989  oexpnegnz  45990  aacllem  47368