Theorem r19.29a 3289

Description: A commonly used pattern in the spirit of r19.29 3254. (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 3287	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3143  df-rex 3144

This theorem is referenced by:  xpdifid  6025  fimaproj  7829  modmuladdnn0  13284  1arith  16263  prmgaplem5  16391  prmgapprmolem  16397  ffthiso  17199  mhmid  18220  mhmmnd  18221  ghmgrp  18223  ghmcmn  18952  ablfac2  19211  ringinvnz1ne0  19342  zringlpirlem1  20631  mp2pm2mplem4  21417  neiptopuni  21738  neiptoptop  21739  neiptopnei  21740  neitr  21788  hauscmplem  22014  2ndcomap  22066  lly1stc  22104  dissnref  22136  neitx  22215  cnextcn  22675  ustexsym  22824  ustex2sym  22825  ustex3sym  22826  trust  22838  utoptop  22843  restutop  22846  restutopopn  22847  ustuqtop1  22850  ustuqtop2  22851  ustuqtop3  22852  ustuqtop4  22853  utopreg  22861  ucncn  22894  fmucnd  22901  cfilufg  22902  trcfilu  22903  neipcfilu  22905  metustid  23164  metustsym  23165  metustexhalf  23166  metust  23168  cfilucfil  23169  metustbl  23176  psmetutop  23177  restmetu  23180  qdensere  23378  opnreen  23439  nmoleub2lem3  23719  ovolicc2lem4  24121  plydivlem4  24885  ulmuni  24980  dchrpt  25843  tgcgrtriv  26270  tgbtwntriv2  26273  tgbtwncom  26274  tgbtwnswapid  26278  tgbtwnintr  26279  tgbtwnouttr2  26281  tgtrisegint  26285  tgifscgr  26294  tgcgrxfr  26304  tgbtwnxfr  26316  motcgrg  26330  tgbtwnconn1lem3  26360  tgbtwnconn1  26361  tgbtwnconn3  26363  legval  26370  legov  26371  legov2  26372  legtrd  26375  legtri3  26376  legtrid  26377  ltgseg  26382  hlcgrex  26402  hlcgreulem  26403  colline  26435  miriso  26456  symquadlem  26475  krippenlem  26476  midexlem  26478  perpneq  26500  isperp2  26501  footexALT  26504  footex  26507  perpdrag  26514  colperpexlem3  26518  colperpex  26519  opphllem  26521  mideulem  26522  midex  26523  oppne3  26529  oppnid  26532  opphllem3  26535  opphllem5  26537  opphllem6  26538  oppperpex  26539  opphl  26540  outpasch  26541  hpgne1  26547  hpgne2  26548  lnopp2hpgb  26549  colopp  26555  lmieu  26570  lnperpex  26589  trgcopy  26590  trgcopyeulem  26591  acopy  26619  acopyeu  26620  inaghl  26631  leagne1  26635  leagne2  26636  leagne3  26637  leagne4  26638  cgrg3col4  26639  tgasa1  26644  f1otrg  26657  ttgbtwnid  26670  cnvbraval  29887  opsqrlem1  29917  rabfodom  30266  acunirnmpt  30404  acunirnmpt2  30405  acunirnmpt2f  30406  xrge0infss  30484  fsumiunle  30545  wrdt2ind  30627  gsummpt2d  30687  trsp2cyc  30765  cycpmrn  30785  tocyccntz  30786  cyc3evpm  30792  cyc3genpm  30794  cycpmgcl  30795  cycpmconjslem2  30797  cyc3conja  30799  archirngz  30818  archiabllem1a  30820  archiabllem1b  30821  archiabllem1  30822  archiabllem2a  30823  archiabllem2c  30824  archiabl  30827  imaslmod  30922  isprmidlc  30963  qsidomlem2  30966  mxidlprm  30977  dimval  31001  dimvalfi  31002  lssdimle  31006  lbsdiflsp0  31022  dimkerim  31023  fedgmul  31027  extdg1id  31053  txomap  31098  qtophaus  31100  pcmplfinf  31125  pstmxmet  31137  pnfneige0  31194  esumcst  31322  esum2d  31352  esumiun  31353  ddemeas  31495  signsply0  31821  signstres  31845  prodfzo03  31874  actfunsnf1o  31875  actfunsnrndisj  31876  tgoldbachgt  31934  poimirlem17  34924  poimirlem20  34927  itg2gt0cn  34962  fdc1  35036  lhprelat3N  37191  dihjat2  38582  prjspersym  39306  eldioph2b  39409  diophrex  39421  irrapxlem6  39473  pellex  39481  pellfundex  39532  lnrfg  39768  mpaaeu  39799  cvgdvgrat  40694  climsuse  41938  limsupre  41971  limcleqr  41974  limsuppnfdlem  42031  limsupub2  42142  xlimclim2lem  42169  climxlim2  42176  cncficcgt0  42220  dvbdfbdioo  42264  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  stoweidlem28  42362  stoweidlem29  42363  stoweidlem52  42386  stoweidlem60  42394  fourierdlem39  42480  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem114  42554  hspmbllem2  42958  nnsum4primesevenALTV  44015