Theorem r19.29a 3198

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2113  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-ral 3058  df-rex 3059

This theorem is referenced by:  xpdifid  5994  fimaproj  7848  modmuladdnn0  13367  1arith  16356  prmgaplem5  16484  prmgapprmolem  16490  ffthiso  17297  mhmid  18331  mhmmnd  18332  ghmgrp  18334  ghmcmn  19064  ablfac2  19323  ringinvnz1ne0  19457  zringlpirlem1  20296  mp2pm2mplem4  21553  neiptopuni  21874  neiptoptop  21875  neiptopnei  21876  neitr  21924  hauscmplem  22150  2ndcomap  22202  lly1stc  22240  dissnref  22272  neitx  22351  cnextcn  22811  ustexsym  22960  ustex2sym  22961  ustex3sym  22962  trust  22974  utoptop  22979  restutop  22982  restutopopn  22983  ustuqtop1  22986  ustuqtop2  22987  ustuqtop3  22988  ustuqtop4  22989  utopreg  22997  ucncn  23030  fmucnd  23037  cfilufg  23038  trcfilu  23039  neipcfilu  23041  metustid  23300  metustsym  23301  metustexhalf  23302  metust  23304  cfilucfil  23305  metustbl  23312  psmetutop  23313  restmetu  23316  qdensere  23515  opnreen  23576  nmoleub2lem3  23860  ovolicc2lem4  24265  plydivlem4  25036  ulmuni  25131  dchrpt  25995  tgcgrtriv  26422  tgbtwntriv2  26425  tgbtwncom  26426  tgbtwnswapid  26430  tgbtwnintr  26431  tgbtwnouttr2  26433  tgtrisegint  26437  tgifscgr  26446  tgcgrxfr  26456  tgbtwnxfr  26468  motcgrg  26482  tgbtwnconn1lem3  26512  tgbtwnconn1  26513  tgbtwnconn3  26515  legval  26522  legov  26523  legov2  26524  legtrd  26527  legtri3  26528  legtrid  26529  ltgseg  26534  hlcgrex  26554  hlcgreulem  26555  colline  26587  miriso  26608  symquadlem  26627  krippenlem  26628  midexlem  26630  perpneq  26652  isperp2  26653  footexALT  26656  footex  26659  perpdrag  26666  colperpexlem3  26670  colperpex  26671  opphllem  26673  mideulem  26674  midex  26675  oppne3  26681  oppnid  26684  opphllem3  26687  opphllem5  26689  opphllem6  26690  oppperpex  26691  opphl  26692  outpasch  26693  hpgne1  26699  hpgne2  26700  lnopp2hpgb  26701  colopp  26707  lmieu  26722  lnperpex  26741  trgcopy  26742  trgcopyeulem  26743  acopy  26771  acopyeu  26772  inaghl  26783  leagne1  26787  leagne2  26788  leagne3  26789  leagne4  26790  cgrg3col4  26791  tgasa1  26796  f1otrg  26809  ttgbtwnid  26822  cnvbraval  30037  opsqrlem1  30067  rabfodom  30417  acunirnmpt  30563  acunirnmpt2  30564  acunirnmpt2f  30565  xrge0infss  30650  fsumiunle  30710  wrdt2ind  30792  mgcf1o  30850  gsummpt2d  30878  trsp2cyc  30959  cycpmrn  30979  tocyccntz  30980  cyc3evpm  30986  cyc3genpm  30988  cycpmgcl  30989  cycpmconjslem2  30991  cyc3conja  30993  archirngz  31012  archiabllem1a  31014  archiabllem1b  31015  archiabllem1  31016  archiabllem2a  31017  archiabllem2c  31018  archiabl  31021  imaslmod  31117  znfermltl  31126  nsgqusf1olem1  31162  rhmimaidl  31173  isprmidlc  31187  qsidomlem2  31193  mxidlprm  31204  dimval  31250  dimvalfi  31251  lssdimle  31255  lbsdiflsp0  31271  dimkerim  31272  fedgmul  31276  extdg1id  31302  txomap  31348  qtophaus  31350  pcmplfinf  31375  zarcls1  31383  zarclsun  31384  zarclsint  31386  zarclssn  31387  zarcmplem  31395  rhmpreimacn  31399  pstmxmet  31411  pnfneige0  31465  esumcst  31593  esum2d  31623  esumiun  31624  ddemeas  31766  signsply0  32092  signstres  32116  prodfzo03  32145  actfunsnf1o  32146  actfunsnrndisj  32147  tgoldbachgt  32205  poimirlem17  35406  poimirlem20  35409  itg2gt0cn  35444  fdc1  35516  lhprelat3N  37666  dihjat2  39057  prjspersym  40007  eldioph2b  40141  diophrex  40153  irrapxlem6  40205  pellex  40213  pellfundex  40264  lnrfg  40500  mpaaeu  40531  cvgdvgrat  41453  climsuse  42675  limsupre  42708  limcleqr  42711  limsuppnfdlem  42768  limsupub2  42879  xlimclim2lem  42906  climxlim2  42913  cncficcgt0  42955  dvbdfbdioo  42997  ioodvbdlimc1lem2  42999  ioodvbdlimc2lem  43001  stoweidlem28  43095  stoweidlem29  43096  stoweidlem52  43119  stoweidlem60  43127  fourierdlem39  43213  fourierdlem102  43275  fourierdlem103  43276  fourierdlem104  43277  fourierdlem114  43287  hspmbllem2  43691  nnsum4primesevenALTV  44771