Theorem r19.29a 3218

Description: A commonly used pattern in the spirit of r19.29 3184. (Contributed by Thierry Arnoux, 22-Nov-2017.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.)

Hypotheses

Ref	Expression
rexlimdva2.1	⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
r19.29a.1	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Assertion

Ref	Expression
r19.29a	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.29a

Step	Hyp	Ref	Expression
1		r19.29a.1	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
2		rexlimdva2.1	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
3	2	rexlimdva2 3216	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 15	1 ⊢ (𝜑 → 𝜒)

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

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 1913

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

This theorem is referenced by:  xpdifid  6071  fimaproj  7976  modmuladdnn0  13635  1arith  16628  prmgaplem5  16756  prmgapprmolem  16762  ffthiso  17645  mhmid  18696  mhmmnd  18697  ghmgrp  18699  ghmcmn  19433  ablfac2  19692  ringinvnz1ne0  19831  zringlpirlem1  20684  mp2pm2mplem4  21958  neiptopuni  22281  neiptoptop  22282  neiptopnei  22283  neitr  22331  hauscmplem  22557  2ndcomap  22609  lly1stc  22647  dissnref  22679  neitx  22758  cnextcn  23218  ustexsym  23367  ustex2sym  23368  ustex3sym  23369  trust  23381  utoptop  23386  restutop  23389  restutopopn  23390  ustuqtop1  23393  ustuqtop2  23394  ustuqtop3  23395  ustuqtop4  23396  utopreg  23404  ucncn  23437  fmucnd  23444  cfilufg  23445  trcfilu  23446  neipcfilu  23448  metustid  23710  metustsym  23711  metustexhalf  23712  metust  23714  cfilucfil  23715  metustbl  23722  psmetutop  23723  restmetu  23726  qdensere  23933  opnreen  23994  nmoleub2lem3  24278  ovolicc2lem4  24684  plydivlem4  25456  ulmuni  25551  dchrpt  26415  tgcgrtriv  26845  tgbtwntriv2  26848  tgbtwncom  26849  tgbtwnswapid  26853  tgbtwnintr  26854  tgbtwnouttr2  26856  tgtrisegint  26860  tgifscgr  26869  tgcgrxfr  26879  tgbtwnxfr  26891  motcgrg  26905  tgbtwnconn1lem3  26935  tgbtwnconn1  26936  tgbtwnconn3  26938  legval  26945  legov  26946  legov2  26947  legtrd  26950  legtri3  26951  legtrid  26952  ltgseg  26957  hlcgrex  26977  hlcgreulem  26978  colline  27010  miriso  27031  symquadlem  27050  krippenlem  27051  midexlem  27053  perpneq  27075  isperp2  27076  footexALT  27079  footex  27082  perpdrag  27089  colperpexlem3  27093  colperpex  27094  opphllem  27096  mideulem  27097  midex  27098  oppne3  27104  oppnid  27107  opphllem3  27110  opphllem5  27112  opphllem6  27113  oppperpex  27114  opphl  27115  outpasch  27116  hpgne1  27122  hpgne2  27123  lnopp2hpgb  27124  colopp  27130  lmieu  27145  lnperpex  27164  trgcopy  27165  trgcopyeulem  27166  acopy  27194  acopyeu  27195  inaghl  27206  leagne1  27210  leagne2  27211  leagne3  27212  leagne4  27213  cgrg3col4  27214  tgasa1  27219  f1otrg  27232  ttgbtwnid  27251  cnvbraval  30472  opsqrlem1  30502  rabfodom  30851  acunirnmpt  30996  acunirnmpt2  30997  acunirnmpt2f  30998  xrge0infss  31083  fsumiunle  31143  wrdt2ind  31225  mgcf1o  31281  gsummpt2d  31309  trsp2cyc  31390  cycpmrn  31410  tocyccntz  31411  cyc3evpm  31417  cyc3genpm  31419  cycpmgcl  31420  cycpmconjslem2  31422  cyc3conja  31424  archirngz  31443  archiabllem1a  31445  archiabllem1b  31446  archiabllem1  31447  archiabllem2a  31448  archiabllem2c  31449  archiabl  31452  imaslmod  31553  znfermltl  31562  nsgqusf1olem1  31598  rhmimaidl  31609  isprmidlc  31623  qsidomlem2  31629  mxidlprm  31640  dimval  31686  dimvalfi  31687  lssdimle  31691  lbsdiflsp0  31707  dimkerim  31708  fedgmul  31712  extdg1id  31738  txomap  31784  qtophaus  31786  pcmplfinf  31811  zarcls1  31819  zarclsun  31820  zarclsint  31822  zarclssn  31823  zarcmplem  31831  rhmpreimacn  31835  pstmxmet  31847  pnfneige0  31901  esumcst  32031  esum2d  32061  esumiun  32062  ddemeas  32204  signsply0  32530  signstres  32554  prodfzo03  32583  actfunsnf1o  32584  actfunsnrndisj  32585  tgoldbachgt  32643  poimirlem17  35794  poimirlem20  35797  itg2gt0cn  35832  fdc1  35904  lhprelat3N  38054  dihjat2  39445  aks4d1p8  40095  prjspersym  40446  eldioph2b  40585  diophrex  40597  irrapxlem6  40649  pellex  40657  pellfundex  40708  lnrfg  40944  mpaaeu  40975  cvgdvgrat  41931  climsuse  43149  limsupre  43182  limcleqr  43185  limsuppnfdlem  43242  limsupub2  43353  xlimclim2lem  43380  climxlim2  43387  cncficcgt0  43429  dvbdfbdioo  43471  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  stoweidlem28  43569  stoweidlem29  43570  stoweidlem52  43593  stoweidlem60  43601  fourierdlem39  43687  fourierdlem102  43749  fourierdlem103  43750  fourierdlem104  43751  fourierdlem114  43761  hspmbllem2  44165  nnsum4primesevenALTV  45253