Theorem rexlimddv 3251

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2079  ∃wrex 3104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-ral 3108  df-rex 3109

This theorem is referenced by:  grprinvlem  7233  grpridd  7235  oaabs2  8113  oemapvali  8982  cantnflem4  8990  r1pwss  9048  djuun  9190  infxpenc2lem1  9280  pwfseqlem3  9917  prlem934  10290  ltexprlem7  10299  reclem3pr  10306  00id  10651  mul02lem1  10652  addid2  10659  addcan  10660  addcan2  10661  negeu  10712  mulcand  11110  suprzcl  11900  uzwo3  12181  expmulnbnd  13434  limsupgre  14660  rlimclim1  14724  fsumcvg3  14907  oexpneg  15515  bitsfi  15607  vdwlem10  16143  mreexexlem4d  16735  mreexdomd  16737  isacs3lem  17593  grprcan  17882  sylow1  18446  pgpfi  18448  slwhash  18467  pj1id  18540  efgsfo  18580  efgredlemc  18586  dmdprdsplitlem  18864  dpjidcl  18885  pgpfac1lem4  18905  pgpfaclem2  18909  pgpfaclem3  18910  gsummgp0  19036  lspsolv  19593  restbas  21438  restcls  21461  restntr  21462  cnpnei  21544  cnpco  21547  pnrmopn  21623  1stcfb  21725  1stcrest  21733  2ndcctbss  21735  2ndcomap  21738  dis2ndc  21740  llyidm  21768  nllyidm  21769  hausllycmp  21774  lly1stc  21776  llycmpkgen2  21830  1stckgenlem  21833  basqtop  21991  regr1lem  22019  kqreglem1  22021  kqreglem2  22022  kqnrmlem1  22023  kqnrmlem2  22024  reghmph  22073  nrmhmph  22074  qtophmeo  22097  trfbas2  22123  fbasfip  22148  fbasrn  22164  trfg  22171  ssufl  22198  fmufil  22239  ufldom  22242  uffclsflim  22311  cnpfcfi  22320  alexsublem  22324  alexsubALTlem4  22330  ptcmplem3  22334  ptcmplem4  22335  tsmsxp  22434  met1stc  22802  met2ndci  22803  prdsxmslem2  22810  metcnpi3  22827  icccmplem1  23101  xrge0tsms  23113  metdseq0  23133  cnllycmp  23231  bndth  23233  lebnumlem1  23236  lebnum  23239  cfilfcls  23548  lmle  23575  relcmpcmet  23592  pjthlem2  23712  ovolscalem2  23786  ovolicc2lem4  23792  ovolicc2lem5  23793  ioombl1  23834  uniioombllem6  23860  uniioombl  23861  opnmbllem  23873  volivth  23879  mbfinf  23937  mbfi1fseqlem6  23992  itg2cnlem1  24033  itg2cn  24035  lhop2  24283  dvcnvre  24287  aareccl  24586  aaliou3lem8  24605  aaliou3lem9  24610  ulmdvlem3  24661  mtestbdd  24664  iblulm  24666  radcnvlem1  24672  abelthlem5  24694  abelthlem8  24698  chordthm  25084  dcubic  25093  lgambdd  25284  lgamucov  25285  lgamcvglem  25287  lgamcvg2  25302  fta  25327  dchrptlem2  25511  sumdchr2  25516  2sqlem11  25675  dchrisum  25738  dchrisum0flb  25756  pntibndlem3  25838  pntlemi  25850  pjspansn  29033  chscllem3  29095  xmulcand  30252  xrge0tsmsd  30460  esumpcvgval  30910  cnpconn  32041  pconnconn  32042  connpconn  32046  pconnpi1  32048  cnllysconn  32056  cvmcov2  32086  cvmliftpht  32129  mthmpps  32382  sinccvg  32469  btwnconn1lem13  33114  neibastop2lem  33262  tailfb  33279  unblimceq0lem  33398  knoppndvlem9  33412  knoppndvlem21  33424  knoppndvlem22  33425  matunitlindflem2  34366  poimirlem29  34398  opnmbllem0  34405  mblfinlem2  34407  mblfinlem4  34409  prdsbnd2  34551  cntotbnd  34552  heiborlem8  34574  heiborlem9  34575  cvlcvr1  35956  llnmlplnN  36156  cdlemb  36411  paddasslem10  36446  trlcnv  36782  trlator0  36788  trlid0  36793  trlnidatb  36794  cdlemd4  36818  cdlemg5  37222  trlco  37344  cdlemj3  37440  tendo0mul  37443  tendo0mulr  37444  tendoconid  37446  erngdv  37610  erngdv-rN  37618  dihmeetlem1N  37907  dihatlat  37951  hgmaprnlem5N  38517  remulcan2d  38633  renegeulemv  38670  prjspertr  38702  0prjspnrel  38716  acongrep  39013  jm2.27b  39039  lmhmfgsplit  39122  hbt  39166  imo72b2lem1  39959  mnuss2d  40049  mnuprdlem4  40060  mnuunid  40062  mnurndlem2  40067  ablsimpgcygd  40116  ablsimpgfindlem1  40117  ablsimpgfind  40119  fincygsubgodexd  40122  ablsimpgprmd  40124  cncmpmax  40780  rexlimddv2  41600  stoweidlem62  41843  oexpnegALTV  43278  oexpnegnz  43279  aacllem  44336