Theorem rexlimddv 3173

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  frxp2  8196  frxp3  8203  oaabs2  8694  oemapvali  9720  cantnflem4  9728  r1pwss  9826  djuun  10042  infxpenc2lem1  10135  pwfseqlem3  10782  prlem934  11155  ltexprlem7  11164  reclem3pr  11171  00id  11522  mul02lem1  11523  addlid  11530  addcan  11531  addcan2  11532  negeu  11584  mulcand  11987  suprzcl  12817  uzwo3  13108  expmulnbnd  14418  limsupgre  15689  rlimclim1  15753  fsumcvg3  15936  oexpneg  16556  bitsfi  16648  vdwlem10  17209  mreexexlem4d  17862  mreexdomd  17864  isacs3lem  18757  grpinvalem  18895  grprida  18897  grprcan  19225  sylow1  19859  pgpfi  19861  slwhash  19880  pj1id  19955  efgsfo  19995  efgredlemc  20001  dmdprdsplitlem  20295  dpjidcl  20316  pgpfac1lem4  20336  pgpfaclem2  20340  pgpfaclem3  20341  ablsimpgcygd  20364  ablsimpgfindlem1  20365  ablsimpgfind  20368  fincygsubgodexd  20371  ablsimpgprmd  20373  gsummgp0  20589  imadrhmcl  21096  lspsolv  21463  matunitlindflem2  23039  restbas  23520  restcls  23543  restntr  23544  cnpnei  23626  cnpco  23629  pnrmopn  23705  1stcfb  23807  1stcrest  23815  2ndcctbss  23818  2ndcomap  23821  dis2ndc  23823  llyidm  23851  nllyidm  23852  hausllycmp  23857  lly1stc  23859  llycmpkgen2  23913  1stckgenlem  23916  basqtop  24074  regr1lem  24102  kqreglem1  24104  kqreglem2  24105  kqnrmlem1  24106  kqnrmlem2  24107  reghmph  24156  nrmhmph  24157  qtophmeo  24180  trfbas2  24206  fbasfip  24231  fbasrn  24247  trfg  24254  ssufl  24281  fmufil  24322  ufldom  24325  uffclsflim  24394  cnpfcfi  24403  alexsublem  24407  alexsubALTlem4  24413  ptcmplem3  24417  ptcmplem4  24418  tsmsxp  24518  met1stc  24884  met2ndci  24885  prdsxmslem2  24892  metcnpi3  24909  icccmplem1  25186  xrge0tsms  25198  metdseq0  25218  cnllycmp  25321  bndth  25323  lebnumlem1  25326  lebnum  25329  cfilfcls  25639  lmle  25666  relcmpcmet  25683  pjthlem2  25803  ovolscalem2  25879  ovolicc2lem4  25885  ovolicc2lem5  25886  ioombl1  25927  uniioombllem6  25953  uniioombl  25954  opnmbllem  25966  volivth  25972  mbfinf  26030  mbfi1fseqlem6  26085  itg2cnlem1  26126  itg2cn  26128  lhop2  26379  dvcnvre  26383  preimaaa  26692  aareccl  26699  aaliou3lem8  26718  aaliou3lem9  26723  ulmdvlem3  26775  mtestbdd  26778  iblulm  26780  radcnvlem1  26786  abelthlem5  26808  abelthlem8  26812  chordthm  27211  dcubic  27220  lgambdd  27410  lgamucov  27411  lgamcvglem  27413  lgamcvg2  27428  fta  27453  dchrptlem2  27638  sumdchr2  27643  2sqlem11  27802  dchrisum  27865  dchrisum0flb  27883  pntibndlem3  27965  pntlemi  27977  cutbdaybnd  28227  cofslts  28350  coinitslts  28351  addsproplem6  28406  negsproplem6  28465  mulsproplem13  28560  mulsproplem14  28561  recsne0  28624  recsex  28651  noseqp1  28723  pjspansn  32225  chscllem3  32287  inagcgratrgxfr  33102  inagcgratrgn  33104  tgextahp  33119  xmulcand  33573  xrge0tsmsd  33723  esumpcvgval  34814  noinfepfnregs  35934  cnpconn  36196  pconnconn  36197  connpconn  36201  pconnpi1  36203  cnllysconn  36211  cvmcov2  36241  cvmliftpht  36284  mthmpps  36548  sinccvg  36639  btwnconn1lem13  37072  neibastop2lem  37356  tailfb  37373  weiunfr  37463  mh-inf3f1  37537  unblimceq0lem  37580  knoppndvlem9  37594  knoppndvlem21  37606  knoppndvlem22  37607  poimirlem29  38828  opnmbllem0  38835  mblfinlem2  38837  mblfinlem4  38839  prdsbnd2  38988  cntotbnd  38989  heiborlem8  39011  heiborlem9  39012  cvlcvr1  40655  llnmlplnN  40855  cdlemb  41110  paddasslem10  41145  trlcnv  41481  trlator0  41487  trlid0  41492  trlnidatb  41493  cdlemd4  41517  cdlemg5  41921  trlco  42043  cdlemj3  42139  tendo0mul  42142  tendo0mulr  42143  tendoconid  42145  erngdv  42309  erngdv-rN  42317  dihmeetlem1N  42606  dihatlat  42650  hgmaprnlem5N  43216  aks6d1c5  43448  remulcan2d  43567  renegeulemv  43679  remul02  43716  remul01  43718  sn-addcand  43731  sn-addrid  43732  sn-addcan2d  43733  sn-subeu  43738  remulinvcom  43744  remullid  43745  remulcand  43750  rediveud  43754  sn-0tie0  43775  imacrhmcl  43841  fiabv  43860  prjspertr  43893  prjspnnorm  43921  0prjspnrel  43923  acongrep  44247  jm2.27b  44273  lmhmfgsplit  44348  hbt  44391  imo72b2lem1  45424  mnuss2d  45503  mnuprdlem4  45514  mnuunid  45516  mnurndlem2  45521  cncmpmax  46317  rexlimddv2  47100  stoweidlem62  47339  salrestss  47638  tmachlem-agreefin  48225  oexpnegALTV  49042  oexpnegnz  49043  upciclem4  50610  aacllem  51361