Theorem r19.29a 3146

Description: A commonly used pattern in the spirit of r19.29 3101. (Contributed by Thierry Arnoux, 22-Nov-2017.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.)

Hypotheses

Ref	Expression
r19.29a.1	⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
r19.29a.2	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Assertion

Ref	Expression
r19.29a	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.29a

Step	Hyp	Ref	Expression
1		r19.29a.2	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
2		r19.29a.1	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
3	2	rexlimdva2 3141	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  xpdifid  6134  fimaproj  8087  modmuladdnn0  13850  1arith  16867  prmgaplem5  16995  prmgapprmolem  17001  ffthiso  17867  chnso  18559  mhmid  19005  mhmmnd  19006  ghmgrp  19008  ghmqusnsg  19223  ghmquskerlem3  19227  ghmqusker  19228  ghmcmn  19772  ablfac2  20032  ringinvnz1ne0  20247  rhmqusnsg  21252  rngqipring1  21283  zringlpirlem1  21429  mp2pm2mplem4  22765  neiptopuni  23086  neiptoptop  23087  neiptopnei  23088  neitr  23136  hauscmplem  23362  2ndcomap  23414  lly1stc  23452  dissnref  23484  neitx  23563  cnextcn  24023  ustexsym  24172  ustex2sym  24173  ustex3sym  24174  trust  24185  utoptop  24190  restutop  24193  restutopopn  24194  ustuqtop1  24197  ustuqtop2  24198  ustuqtop3  24199  ustuqtop4  24200  utopreg  24208  ucncn  24240  fmucnd  24247  cfilufg  24248  trcfilu  24249  neipcfilu  24251  metustid  24510  metustsym  24511  metustexhalf  24512  metust  24514  cfilucfil  24515  metustbl  24522  psmetutop  24523  restmetu  24526  qdensere  24725  opnreen  24788  nmoleub2lem3  25083  ovolicc2lem4  25489  plydivlem4  26272  ulmuni  26369  dchrpt  27246  tgcgrtriv  28568  tgbtwntriv2  28571  tgbtwncom  28572  tgbtwnswapid  28576  tgbtwnintr  28577  tgbtwnouttr2  28579  tgtrisegint  28583  tgifscgr  28592  tgcgrxfr  28602  tgbtwnxfr  28614  motcgrg  28628  tgbtwnconn1lem3  28658  tgbtwnconn1  28659  tgbtwnconn3  28661  legval  28668  legov  28669  legov2  28670  legtrd  28673  legtri3  28674  legtrid  28675  ltgseg  28680  hlcgrex  28700  hlcgreulem  28701  colline  28733  miriso  28754  symquadlem  28773  krippenlem  28774  midexlem  28776  perpneq  28798  isperp2  28799  footexALT  28802  footex  28805  perpdrag  28812  colperpexlem3  28816  colperpex  28817  opphllem  28819  mideulem  28820  midex  28821  oppne3  28827  oppnid  28830  opphllem3  28833  opphllem5  28835  opphllem6  28836  oppperpex  28837  opphl  28838  outpasch  28839  hpgne1  28845  hpgne2  28846  lnopp2hpgb  28847  colopp  28853  lmieu  28868  lnperpex  28887  trgcopy  28888  trgcopyeulem  28889  acopy  28917  acopyeu  28918  inaghl  28929  leagne1  28933  leagne2  28934  leagne3  28935  leagne4  28936  cgrg3col4  28937  tgasa1  28942  f1otrg  28955  ttgbtwnid  28968  cnvbraval  32197  opsqrlem1  32227  rabfodom  32591  acunirnmpt  32748  acunirnmpt2  32749  acunirnmpt2f  32750  xrge0infss  32850  fsumiunle  32920  2exple2exp  32936  expevenpos  32937  wrdt2ind  33045  mgcf1o  33095  mndlactf1o  33122  gsummpt2d  33142  gsumwrd2dccatlem  33170  trsp2cyc  33216  cycpmrn  33236  tocyccntz  33237  cyc3evpm  33243  cyc3genpm  33245  cycpmgcl  33246  cycpmconjslem2  33248  cyc3conja  33250  archirngz  33282  archiabllem1a  33284  archiabllem1b  33285  archiabllem1  33286  archiabllem2a  33287  archiabllem2c  33288  archiabl  33291  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem4  33338  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  elrgspnsubrun  33342  erler  33358  elrlocbasi  33359  rlocaddval  33361  rlocmulval  33362  rlocf1  33366  isdrng4  33388  fracfld  33401  imaslmod  33445  znfermltl  33458  nsgqusf1olem1  33505  lmhmqusker  33509  unitpidl1  33516  rhmquskerlem  33517  rhmimaidl  33524  drngidl  33525  isprmidlc  33539  qsidomlem2  33545  ssdifidlprm  33550  mxidlprm  33562  mxidlirredi  33563  mxidlirred  33564  drngmxidlr  33570  opprqusplusg  33581  opprqusmulr  33583  qsdrngi  33587  qsdrnglem2  33588  rprmasso2  33618  rprmirredlem  33622  1arithidom  33629  pidufd  33635  1arithufdlem1  33636  1arithufdlem2  33637  1arithufdlem3  33638  1arithufdlem4  33639  dfufd2lem  33641  dfufd2  33642  esplymhp  33744  esplyfv1  33745  esplyfv  33746  esplyfval3  33748  esplyfval1  33749  lbslelsp  33774  dimval  33777  dimvalfi  33778  lssdimle  33784  lbsdiflsp0  33803  dimkerim  33804  fedgmul  33808  dimlssid  33809  extdg1id  33843  fldextrspunlsplem  33850  extdgfialglem1  33869  extdgfialg  33871  irngnminplynz  33889  fldext2chn  33905  constrext2chnlem  33927  constrfiss  33928  constrllcllem  33929  constrlccllem  33930  constrcccllem  33931  constrcn  33937  cos9thpiminplylem2  33960  txomap  34011  qtophaus  34013  pcmplfinf  34038  zarcls1  34046  zarclsun  34047  zarclsint  34049  zarclssn  34050  zarcmplem  34058  rhmpreimacn  34062  pstmxmet  34074  pnfneige0  34128  esumcst  34240  esum2d  34270  esumiun  34271  ddemeas  34413  signsply0  34728  signstres  34752  prodfzo03  34780  actfunsnf1o  34781  actfunsnrndisj  34782  tgoldbachgt  34840  poimirlem17  37885  poimirlem20  37888  itg2gt0cn  37923  fdc1  37994  lhprelat3N  40413  dihjat2  41804  aks4d1p8  42454  primrootspoweq0  42473  aks6d1c4  42491  aks6d1c6isolem1  42541  aks6d1c6isolem2  42542  aks6d1c6lem5  42544  aks6d1c7  42551  rhmqusspan  42552  grpods  42561  unitscyglem1  42562  unitscyglem2  42563  unitscyglem3  42564  unitscyglem4  42565  aks5lem7  42567  aks5  42571  prjspersym  42962  eldioph2b  43117  diophrex  43129  irrapxlem6  43181  pellex  43189  pellfundex  43240  lnrfg  43473  mpaaeu  43504  cvgdvgrat  44666  climsuse  45965  limsupre  45996  limcleqr  45999  limsuppnfdlem  46056  liminflelimsuplem  46130  limsupub2  46167  xlimclim2lem  46194  climxlim2  46201  cncficcgt0  46243  dvbdfbdioo  46285  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  stoweidlem28  46383  stoweidlem29  46384  stoweidlem52  46407  stoweidlem60  46415  fourierdlem39  46501  fourierdlem102  46563  fourierdlem103  46564  fourierdlem104  46565  fourierdlem114  46575  hspmbllem2  46982  nnsum4primesevenALTV  48158  imaf1co  49511