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 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

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

This theorem is referenced by:  frxp2  8141  frxp3  8148  oaabs2  8636  oemapvali  9654  cantnflem4  9662  r1pwss  9757  djuun  9913  infxpenc2lem1  10004  pwfseqlem3  10646  prlem934  11019  ltexprlem7  11028  reclem3pr  11035  00id  11386  mul02lem1  11387  addlid  11394  addcan  11395  addcan2  11396  negeu  11448  mulcand  11848  suprzcl  12677  uzwo3  12968  expmulnbnd  14273  limsupgre  15534  rlimclim1  15598  fsumcvg3  15782  oexpneg  16404  bitsfi  16496  vdwlem10  17051  mreexexlem4d  17704  mreexdomd  17706  isacs3lem  18599  grpinvalem  18732  grprida  18734  grprcan  19041  sylow1  19674  pgpfi  19676  slwhash  19695  pj1id  19770  efgsfo  19810  efgredlemc  19816  dmdprdsplitlem  20110  dpjidcl  20131  pgpfac1lem4  20151  pgpfaclem2  20155  pgpfaclem3  20156  ablsimpgcygd  20179  ablsimpgfindlem1  20180  ablsimpgfind  20183  fincygsubgodexd  20186  ablsimpgprmd  20188  gsummgp0  20400  imadrhmcl  20881  lspsolv  21248  restbas  23296  restcls  23319  restntr  23320  cnpnei  23402  cnpco  23405  pnrmopn  23481  1stcfb  23583  1stcrest  23591  2ndcctbss  23593  2ndcomap  23596  dis2ndc  23598  llyidm  23626  nllyidm  23627  hausllycmp  23632  lly1stc  23634  llycmpkgen2  23688  1stckgenlem  23691  basqtop  23849  regr1lem  23877  kqreglem1  23879  kqreglem2  23880  kqnrmlem1  23881  kqnrmlem2  23882  reghmph  23931  nrmhmph  23932  qtophmeo  23955  trfbas2  23981  fbasfip  24006  fbasrn  24022  trfg  24029  ssufl  24056  fmufil  24097  ufldom  24100  uffclsflim  24169  cnpfcfi  24178  alexsublem  24182  alexsubALTlem4  24188  ptcmplem3  24192  ptcmplem4  24193  tsmsxp  24293  met1stc  24659  met2ndci  24660  prdsxmslem2  24667  metcnpi3  24684  icccmplem1  24961  xrge0tsms  24973  metdseq0  24993  cnllycmp  25096  bndth  25098  lebnumlem1  25101  lebnum  25104  cfilfcls  25414  lmle  25441  relcmpcmet  25458  pjthlem2  25578  ovolscalem2  25654  ovolicc2lem4  25660  ovolicc2lem5  25661  ioombl1  25702  uniioombllem6  25728  uniioombl  25729  opnmbllem  25741  volivth  25747  mbfinf  25805  mbfi1fseqlem6  25860  itg2cnlem1  25901  itg2cn  25903  lhop2  26155  dvcnvre  26159  aareccl  26470  aaliou3lem8  26489  aaliou3lem9  26494  ulmdvlem3  26546  mtestbdd  26549  iblulm  26551  radcnvlem1  26557  abelthlem5  26579  abelthlem8  26583  chordthm  26983  dcubic  26992  lgambdd  27182  lgamucov  27183  lgamcvglem  27185  lgamcvg2  27200  fta  27225  dchrptlem2  27410  sumdchr2  27415  2sqlem11  27574  dchrisum  27637  dchrisum0flb  27655  pntibndlem3  27737  pntlemi  27749  cutbdaybnd  27969  cofslts  28092  coinitslts  28093  addsproplem6  28148  negsproplem6  28207  mulsproplem13  28302  mulsproplem14  28303  recsne0  28366  recsex  28393  noseqp1  28465  pjspansn  31910  chscllem3  31972  xmulcand  33221  xrge0tsmsd  33374  esumpcvgval  34449  noinfepfnregs  35526  cnpconn  35703  pconnconn  35704  connpconn  35708  pconnpi1  35710  cnllysconn  35718  cvmcov2  35748  cvmliftpht  35791  mthmpps  36055  sinccvg  36146  btwnconn1lem13  36572  neibastop2lem  36852  tailfb  36869  weiunfr  36959  unblimceq0lem  37076  knoppndvlem9  37090  knoppndvlem21  37102  knoppndvlem22  37103  matunitlindflem2  38249  poimirlem29  38281  opnmbllem0  38288  mblfinlem2  38290  mblfinlem4  38292  prdsbnd2  38427  cntotbnd  38428  heiborlem8  38450  heiborlem9  38451  cvlcvr1  40094  llnmlplnN  40294  cdlemb  40549  paddasslem10  40584  trlcnv  40920  trlator0  40926  trlid0  40931  trlnidatb  40932  cdlemd4  40956  cdlemg5  41360  trlco  41482  cdlemj3  41578  tendo0mul  41581  tendo0mulr  41582  tendoconid  41584  erngdv  41748  erngdv-rN  41756  dihmeetlem1N  42045  dihatlat  42089  hgmaprnlem5N  42655  aks6d1c5  42887  remulcan2d  43005  renegeulemv  43110  remul02  43147  remul01  43149  sn-addcand  43162  sn-addrid  43163  sn-addcan2d  43164  sn-subeu  43169  remulinvcom  43175  remullid  43176  remulcand  43181  rediveud  43185  sn-0tie0  43206  imacrhmcl  43269  fiabv  43287  prjspertr  43320  0prjspnrel  43342  acongrep  43690  jm2.27b  43716  lmhmfgsplit  43796  hbt  43840  imo72b2lem1  44878  mnuss2d  44957  mnuprdlem4  44968  mnuunid  44970  mnurndlem2  44975  cncmpmax  45735  rexlimddv2  46520  stoweidlem62  46759  salrestss  47058  oexpnegALTV  48425  oexpnegnz  48426  upciclem4  49930  aacllem  50584