Theorem r19.29a 3228

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

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2048  ∃wrex 3083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-ral 3087  df-rex 3088

This theorem is referenced by:  xpdifid  5859  modmuladdnn0  13091  1arith  16109  prmgaplem5  16237  prmgapprmolem  16243  ffthiso  17047  mhmid  17997  mhmmnd  17998  ghmgrp  18000  ghmcmn  18700  ablfac2  18951  ringinvnz1ne0  19055  zringlpirlem1  20323  mp2pm2mplem4  21111  neiptopuni  21432  neiptoptop  21433  neiptopnei  21434  neitr  21482  hauscmplem  21708  2ndcomap  21760  lly1stc  21798  dissnref  21830  neitx  21909  cnextcn  22369  ustexsym  22517  ustex2sym  22518  ustex3sym  22519  trust  22531  utoptop  22536  restutop  22539  restutopopn  22540  ustuqtop1  22543  ustuqtop2  22544  ustuqtop3  22545  ustuqtop4  22546  utopreg  22554  ucncn  22587  fmucnd  22594  cfilufg  22595  trcfilu  22596  neipcfilu  22598  metustid  22857  metustsym  22858  metustexhalf  22859  metust  22861  cfilucfil  22862  metustbl  22869  psmetutop  22870  restmetu  22873  qdensere  23071  opnreen  23132  nmoleub2lem3  23412  ovolicc2lem4  23814  plydivlem4  24578  ulmuni  24673  dchrpt  25535  tgcgrtriv  25962  tgbtwntriv2  25965  tgbtwncom  25966  tgbtwnswapid  25970  tgbtwnintr  25971  tgbtwnouttr2  25973  tgtrisegint  25977  tgifscgr  25986  tgcgrxfr  25996  tgbtwnxfr  26008  motcgrg  26022  tgbtwnconn1lem3  26052  tgbtwnconn1  26053  tgbtwnconn3  26055  legval  26062  legov  26063  legov2  26064  legtrd  26067  legtri3  26068  legtrid  26069  ltgseg  26074  hlcgrex  26094  hlcgreulem  26095  colline  26127  miriso  26148  symquadlem  26167  krippenlem  26168  midexlem  26170  perpneq  26192  isperp2  26193  footexALT  26196  footex  26199  perpdrag  26206  colperpexlem3  26210  colperpex  26211  opphllem  26213  mideulem  26214  midex  26215  oppne3  26221  oppnid  26224  opphllem3  26227  opphllem5  26229  opphllem6  26230  oppperpex  26231  opphl  26232  outpasch  26233  hpgne1  26239  hpgne2  26240  lnopp2hpgb  26241  colopp  26247  lmieu  26262  lnperpex  26281  trgcopy  26282  trgcopyeulem  26283  acopy  26312  acopyeu  26313  inaghl  26324  leagne1  26328  leagne2  26329  leagne3  26330  leagne4  26331  cgrg3col4  26332  tgasa1  26337  f1otrg  26350  ttgbtwnid  26363  cnvbraval  29658  opsqrlem1  29688  rabfodom  30035  acunirnmpt  30156  acunirnmpt2  30157  acunirnmpt2f  30158  xrge0infss  30225  fsumiunle  30280  archirngz  30440  archiabllem1a  30442  archiabllem1b  30443  archiabllem1  30444  archiabllem2a  30445  archiabllem2c  30446  archiabl  30449  gsummpt2d  30480  imaslmod  30557  dimval  30586  dimvalfi  30587  lssdimle  30591  lbsdiflsp0  30607  dimkerim  30608  fedgmul  30612  extdg1id  30638  fimaproj  30698  txomap  30699  qtophaus  30701  pcmplfinf  30726  pstmxmet  30738  pnfneige0  30795  esumcst  30923  esum2d  30953  esumiun  30954  ddemeas  31097  signsply0  31428  signstres  31453  prodfzo03  31483  actfunsnf1o  31484  actfunsnrndisj  31485  tgoldbachgt  31543  poimirlem17  34298  poimirlem20  34301  itg2gt0cn  34336  fdc1  34411  lhprelat3N  36569  dihjat2  37960  prjspersym  38609  eldioph2b  38700  diophrex  38713  irrapxlem6  38765  pellex  38773  pellfundex  38824  lnrfg  39060  mpaaeu  39091  cvgdvgrat  40005  climsuse  41266  limsupre  41299  limcleqr  41302  limsupub2  41470  xlimclim2lem  41497  climxlim2  41504  cncficcgt0  41547  dvbdfbdioo  41591  ioodvbdlimc1lem2  41593  ioodvbdlimc2lem  41595  stoweidlem28  41690  stoweidlem29  41691  stoweidlem52  41714  stoweidlem60  41722  fourierdlem39  41808  fourierdlem102  41870  fourierdlem103  41871  fourierdlem104  41872  fourierdlem114  41882  hspmbllem2  42286  nnsum4primesevenALTV  43274