Theorem r19.29a 3248

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∃wrex 3107

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  xpdifid  5992  fimaproj  7812  modmuladdnn0  13278  1arith  16253  prmgaplem5  16381  prmgapprmolem  16387  ffthiso  17191  mhmid  18212  mhmmnd  18213  ghmgrp  18215  ghmcmn  18945  ablfac2  19204  ringinvnz1ne0  19338  zringlpirlem1  20177  mp2pm2mplem4  21414  neiptopuni  21735  neiptoptop  21736  neiptopnei  21737  neitr  21785  hauscmplem  22011  2ndcomap  22063  lly1stc  22101  dissnref  22133  neitx  22212  cnextcn  22672  ustexsym  22821  ustex2sym  22822  ustex3sym  22823  trust  22835  utoptop  22840  restutop  22843  restutopopn  22844  ustuqtop1  22847  ustuqtop2  22848  ustuqtop3  22849  ustuqtop4  22850  utopreg  22858  ucncn  22891  fmucnd  22898  cfilufg  22899  trcfilu  22900  neipcfilu  22902  metustid  23161  metustsym  23162  metustexhalf  23163  metust  23165  cfilucfil  23166  metustbl  23173  psmetutop  23174  restmetu  23177  qdensere  23375  opnreen  23436  nmoleub2lem3  23720  ovolicc2lem4  24124  plydivlem4  24892  ulmuni  24987  dchrpt  25851  tgcgrtriv  26278  tgbtwntriv2  26281  tgbtwncom  26282  tgbtwnswapid  26286  tgbtwnintr  26287  tgbtwnouttr2  26289  tgtrisegint  26293  tgifscgr  26302  tgcgrxfr  26312  tgbtwnxfr  26324  motcgrg  26338  tgbtwnconn1lem3  26368  tgbtwnconn1  26369  tgbtwnconn3  26371  legval  26378  legov  26379  legov2  26380  legtrd  26383  legtri3  26384  legtrid  26385  ltgseg  26390  hlcgrex  26410  hlcgreulem  26411  colline  26443  miriso  26464  symquadlem  26483  krippenlem  26484  midexlem  26486  perpneq  26508  isperp2  26509  footexALT  26512  footex  26515  perpdrag  26522  colperpexlem3  26526  colperpex  26527  opphllem  26529  mideulem  26530  midex  26531  oppne3  26537  oppnid  26540  opphllem3  26543  opphllem5  26545  opphllem6  26546  oppperpex  26547  opphl  26548  outpasch  26549  hpgne1  26555  hpgne2  26556  lnopp2hpgb  26557  colopp  26563  lmieu  26578  lnperpex  26597  trgcopy  26598  trgcopyeulem  26599  acopy  26627  acopyeu  26628  inaghl  26639  leagne1  26643  leagne2  26644  leagne3  26645  leagne4  26646  cgrg3col4  26647  tgasa1  26652  f1otrg  26665  ttgbtwnid  26678  cnvbraval  29893  opsqrlem1  29923  rabfodom  30274  acunirnmpt  30422  acunirnmpt2  30423  acunirnmpt2f  30424  xrge0infss  30510  fsumiunle  30571  wrdt2ind  30653  gsummpt2d  30734  trsp2cyc  30815  cycpmrn  30835  tocyccntz  30836  cyc3evpm  30842  cyc3genpm  30844  cycpmgcl  30845  cycpmconjslem2  30847  cyc3conja  30849  archirngz  30868  archiabllem1a  30870  archiabllem1b  30871  archiabllem1  30872  archiabllem2a  30873  archiabllem2c  30874  archiabl  30877  imaslmod  30973  rhmimaidl  31017  isprmidlc  31031  qsidomlem2  31037  mxidlprm  31048  dimval  31089  dimvalfi  31090  lssdimle  31094  lbsdiflsp0  31110  dimkerim  31111  fedgmul  31115  extdg1id  31141  txomap  31187  qtophaus  31189  pcmplfinf  31214  zarcls1  31222  zarclsun  31223  zarclsint  31225  zarclssn  31226  zarcmplem  31234  rhmpreimacn  31238  pstmxmet  31250  pnfneige0  31304  esumcst  31432  esum2d  31462  esumiun  31463  ddemeas  31605  signsply0  31931  signstres  31955  prodfzo03  31984  actfunsnf1o  31985  actfunsnrndisj  31986  tgoldbachgt  32044  poimirlem17  35074  poimirlem20  35077  itg2gt0cn  35112  fdc1  35184  lhprelat3N  37336  dihjat2  38727  prjspersym  39601  eldioph2b  39704  diophrex  39716  irrapxlem6  39768  pellex  39776  pellfundex  39827  lnrfg  40063  mpaaeu  40094  cvgdvgrat  41017  climsuse  42250  limsupre  42283  limcleqr  42286  limsuppnfdlem  42343  limsupub2  42454  xlimclim2lem  42481  climxlim2  42488  cncficcgt0  42530  dvbdfbdioo  42572  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  stoweidlem28  42670  stoweidlem29  42671  stoweidlem52  42694  stoweidlem60  42702  fourierdlem39  42788  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem114  42862  hspmbllem2  43266  nnsum4primesevenALTV  44319