Theorem rexlimddv 3221

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3070  df-rex 3071

This theorem is referenced by:  oaabs2  8488  oemapvali  9451  cantnflem4  9459  r1pwss  9551  djuun  9693  infxpenc2lem1  9784  pwfseqlem3  10425  prlem934  10798  ltexprlem7  10807  reclem3pr  10814  00id  11159  mul02lem1  11160  addid2  11167  addcan  11168  addcan2  11169  negeu  11220  mulcand  11617  suprzcl  12409  uzwo3  12692  expmulnbnd  13959  limsupgre  15199  rlimclim1  15263  fsumcvg3  15450  oexpneg  16063  bitsfi  16153  vdwlem10  16700  mreexexlem4d  17365  mreexdomd  17367  isacs3lem  18269  grprinvlem  18366  grpridd  18368  grprcan  18622  sylow1  19217  pgpfi  19219  slwhash  19238  pj1id  19314  efgsfo  19354  efgredlemc  19360  dmdprdsplitlem  19649  dpjidcl  19670  pgpfac1lem4  19690  pgpfaclem2  19694  pgpfaclem3  19695  ablsimpgcygd  19718  ablsimpgfindlem1  19719  ablsimpgfind  19722  fincygsubgodexd  19725  ablsimpgprmd  19727  gsummgp0  19856  lspsolv  20414  restbas  22318  restcls  22341  restntr  22342  cnpnei  22424  cnpco  22427  pnrmopn  22503  1stcfb  22605  1stcrest  22613  2ndcctbss  22615  2ndcomap  22618  dis2ndc  22620  llyidm  22648  nllyidm  22649  hausllycmp  22654  lly1stc  22656  llycmpkgen2  22710  1stckgenlem  22713  basqtop  22871  regr1lem  22899  kqreglem1  22901  kqreglem2  22902  kqnrmlem1  22903  kqnrmlem2  22904  reghmph  22953  nrmhmph  22954  qtophmeo  22977  trfbas2  23003  fbasfip  23028  fbasrn  23044  trfg  23051  ssufl  23078  fmufil  23119  ufldom  23122  uffclsflim  23191  cnpfcfi  23200  alexsublem  23204  alexsubALTlem4  23210  ptcmplem3  23214  ptcmplem4  23215  tsmsxp  23315  met1stc  23686  met2ndci  23687  prdsxmslem2  23694  metcnpi3  23711  icccmplem1  23994  xrge0tsms  24006  metdseq0  24026  cnllycmp  24128  bndth  24130  lebnumlem1  24133  lebnum  24136  cfilfcls  24447  lmle  24474  relcmpcmet  24491  pjthlem2  24611  ovolscalem2  24687  ovolicc2lem4  24693  ovolicc2lem5  24694  ioombl1  24735  uniioombllem6  24761  uniioombl  24762  opnmbllem  24774  volivth  24780  mbfinf  24838  mbfi1fseqlem6  24894  itg2cnlem1  24935  itg2cn  24937  lhop2  25188  dvcnvre  25192  aareccl  25495  aaliou3lem8  25514  aaliou3lem9  25519  ulmdvlem3  25570  mtestbdd  25573  iblulm  25575  radcnvlem1  25581  abelthlem5  25603  abelthlem8  25607  chordthm  25996  dcubic  26005  lgambdd  26195  lgamucov  26196  lgamcvglem  26198  lgamcvg2  26213  fta  26238  dchrptlem2  26422  sumdchr2  26427  2sqlem11  26586  dchrisum  26649  dchrisum0flb  26667  pntibndlem3  26749  pntlemi  26761  pjspansn  29948  chscllem3  30010  xmulcand  31204  xrge0tsmsd  31326  esumpcvgval  32055  cnpconn  33201  pconnconn  33202  connpconn  33206  pconnpi1  33208  cnllysconn  33216  cvmcov2  33246  cvmliftpht  33289  mthmpps  33553  sinccvg  33640  frxp2  33800  frxp3  33806  scutbdaybnd  34018  cofsslt  34097  coinitsslt  34098  btwnconn1lem13  34410  neibastop2lem  34558  tailfb  34575  unblimceq0lem  34695  knoppndvlem9  34709  knoppndvlem21  34721  knoppndvlem22  34722  matunitlindflem2  35783  poimirlem29  35815  opnmbllem0  35822  mblfinlem2  35824  mblfinlem4  35826  prdsbnd2  35962  cntotbnd  35963  heiborlem8  35985  heiborlem9  35986  cvlcvr1  37360  llnmlplnN  37560  cdlemb  37815  paddasslem10  37850  trlcnv  38186  trlator0  38192  trlid0  38197  trlnidatb  38198  cdlemd4  38222  cdlemg5  38626  trlco  38748  cdlemj3  38844  tendo0mul  38847  tendo0mulr  38848  tendoconid  38850  erngdv  39014  erngdv-rN  39022  dihmeetlem1N  39311  dihatlat  39355  hgmaprnlem5N  39921  remulcan2d  40300  renegeulemv  40358  remul02  40395  remul01  40397  sn-addcand  40408  sn-addid1  40409  sn-addcan2d  40410  sn-subeu  40415  remulinvcom  40421  remulid2  40422  remulcand  40427  sn-0tie0  40428  itrere  40443  retire  40444  prjspertr  40451  0prjspnrel  40471  prjcrv0  40477  acongrep  40809  jm2.27b  40835  lmhmfgsplit  40918  hbt  40962  imo72b2lem1  41787  mnuss2d  41889  mnuprdlem4  41900  mnuunid  41902  mnurndlem2  41907  cncmpmax  42582  rexlimddv2  43371  stoweidlem62  43610  oexpnegALTV  45140  oexpnegnz  45141  aacllem  46516