Theorem r19.29a 3217

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  xpdifid  6060  fimaproj  7947  modmuladdnn0  13563  1arith  16556  prmgaplem5  16684  prmgapprmolem  16690  ffthiso  17561  mhmid  18611  mhmmnd  18612  ghmgrp  18614  ghmcmn  19348  ablfac2  19607  ringinvnz1ne0  19746  zringlpirlem1  20596  mp2pm2mplem4  21866  neiptopuni  22189  neiptoptop  22190  neiptopnei  22191  neitr  22239  hauscmplem  22465  2ndcomap  22517  lly1stc  22555  dissnref  22587  neitx  22666  cnextcn  23126  ustexsym  23275  ustex2sym  23276  ustex3sym  23277  trust  23289  utoptop  23294  restutop  23297  restutopopn  23298  ustuqtop1  23301  ustuqtop2  23302  ustuqtop3  23303  ustuqtop4  23304  utopreg  23312  ucncn  23345  fmucnd  23352  cfilufg  23353  trcfilu  23354  neipcfilu  23356  metustid  23616  metustsym  23617  metustexhalf  23618  metust  23620  cfilucfil  23621  metustbl  23628  psmetutop  23629  restmetu  23632  qdensere  23839  opnreen  23900  nmoleub2lem3  24184  ovolicc2lem4  24589  plydivlem4  25361  ulmuni  25456  dchrpt  26320  tgcgrtriv  26749  tgbtwntriv2  26752  tgbtwncom  26753  tgbtwnswapid  26757  tgbtwnintr  26758  tgbtwnouttr2  26760  tgtrisegint  26764  tgifscgr  26773  tgcgrxfr  26783  tgbtwnxfr  26795  motcgrg  26809  tgbtwnconn1lem3  26839  tgbtwnconn1  26840  tgbtwnconn3  26842  legval  26849  legov  26850  legov2  26851  legtrd  26854  legtri3  26855  legtrid  26856  ltgseg  26861  hlcgrex  26881  hlcgreulem  26882  colline  26914  miriso  26935  symquadlem  26954  krippenlem  26955  midexlem  26957  perpneq  26979  isperp2  26980  footexALT  26983  footex  26986  perpdrag  26993  colperpexlem3  26997  colperpex  26998  opphllem  27000  mideulem  27001  midex  27002  oppne3  27008  oppnid  27011  opphllem3  27014  opphllem5  27016  opphllem6  27017  oppperpex  27018  opphl  27019  outpasch  27020  hpgne1  27026  hpgne2  27027  lnopp2hpgb  27028  colopp  27034  lmieu  27049  lnperpex  27068  trgcopy  27069  trgcopyeulem  27070  acopy  27098  acopyeu  27099  inaghl  27110  leagne1  27114  leagne2  27115  leagne3  27116  leagne4  27117  cgrg3col4  27118  tgasa1  27123  f1otrg  27136  ttgbtwnid  27154  cnvbraval  30373  opsqrlem1  30403  rabfodom  30752  acunirnmpt  30898  acunirnmpt2  30899  acunirnmpt2f  30900  xrge0infss  30985  fsumiunle  31045  wrdt2ind  31127  mgcf1o  31183  gsummpt2d  31211  trsp2cyc  31292  cycpmrn  31312  tocyccntz  31313  cyc3evpm  31319  cyc3genpm  31321  cycpmgcl  31322  cycpmconjslem2  31324  cyc3conja  31326  archirngz  31345  archiabllem1a  31347  archiabllem1b  31348  archiabllem1  31349  archiabllem2a  31350  archiabllem2c  31351  archiabl  31354  imaslmod  31455  znfermltl  31464  nsgqusf1olem1  31500  rhmimaidl  31511  isprmidlc  31525  qsidomlem2  31531  mxidlprm  31542  dimval  31588  dimvalfi  31589  lssdimle  31593  lbsdiflsp0  31609  dimkerim  31610  fedgmul  31614  extdg1id  31640  txomap  31686  qtophaus  31688  pcmplfinf  31713  zarcls1  31721  zarclsun  31722  zarclsint  31724  zarclssn  31725  zarcmplem  31733  rhmpreimacn  31737  pstmxmet  31749  pnfneige0  31803  esumcst  31931  esum2d  31961  esumiun  31962  ddemeas  32104  signsply0  32430  signstres  32454  prodfzo03  32483  actfunsnf1o  32484  actfunsnrndisj  32485  tgoldbachgt  32543  poimirlem17  35721  poimirlem20  35724  itg2gt0cn  35759  fdc1  35831  lhprelat3N  37981  dihjat2  39372  aks4d1p8  40023  prjspersym  40367  eldioph2b  40501  diophrex  40513  irrapxlem6  40565  pellex  40573  pellfundex  40624  lnrfg  40860  mpaaeu  40891  cvgdvgrat  41820  climsuse  43039  limsupre  43072  limcleqr  43075  limsuppnfdlem  43132  limsupub2  43243  xlimclim2lem  43270  climxlim2  43277  cncficcgt0  43319  dvbdfbdioo  43361  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem28  43459  stoweidlem29  43460  stoweidlem52  43483  stoweidlem60  43491  fourierdlem39  43577  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  hspmbllem2  44055  nnsum4primesevenALTV  45141