Theorem r19.29a 3145

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

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

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 3062

This theorem is referenced by:  xpdifid  6132  fimaproj  8085  modmuladdnn0  13877  1arith  16898  prmgaplem5  17026  prmgapprmolem  17032  ffthiso  17898  chnso  18590  mhmid  19039  mhmmnd  19040  ghmgrp  19042  ghmqusnsg  19257  ghmquskerlem3  19261  ghmqusker  19262  ghmcmn  19806  ablfac2  20066  ringinvnz1ne0  20281  rhmqusnsg  21283  rngqipring1  21314  zringlpirlem1  21442  mp2pm2mplem4  22774  neiptopuni  23095  neiptoptop  23096  neiptopnei  23097  neitr  23145  hauscmplem  23371  2ndcomap  23423  lly1stc  23461  dissnref  23493  neitx  23572  cnextcn  24032  ustexsym  24181  ustex2sym  24182  ustex3sym  24183  trust  24194  utoptop  24199  restutop  24202  restutopopn  24203  ustuqtop1  24206  ustuqtop2  24207  ustuqtop3  24208  ustuqtop4  24209  utopreg  24217  ucncn  24249  fmucnd  24256  cfilufg  24257  trcfilu  24258  neipcfilu  24260  metustid  24519  metustsym  24520  metustexhalf  24521  metust  24523  cfilucfil  24524  metustbl  24531  psmetutop  24532  restmetu  24535  qdensere  24734  opnreen  24797  nmoleub2lem3  25082  ovolicc2lem4  25487  plydivlem4  26262  ulmuni  26357  dchrpt  27230  tgcgrtriv  28552  tgbtwntriv2  28555  tgbtwncom  28556  tgbtwnswapid  28560  tgbtwnintr  28561  tgbtwnouttr2  28563  tgtrisegint  28567  tgifscgr  28576  tgcgrxfr  28586  tgbtwnxfr  28598  motcgrg  28612  tgbtwnconn1lem3  28642  tgbtwnconn1  28643  tgbtwnconn3  28645  legval  28652  legov  28653  legov2  28654  legtrd  28657  legtri3  28658  legtrid  28659  ltgseg  28664  hlcgrex  28684  hlcgreulem  28685  colline  28717  miriso  28738  symquadlem  28757  krippenlem  28758  midexlem  28760  perpneq  28782  isperp2  28783  footexALT  28786  footex  28789  perpdrag  28796  colperpexlem3  28800  colperpex  28801  opphllem  28803  mideulem  28804  midex  28805  oppne3  28811  oppnid  28814  opphllem3  28817  opphllem5  28819  opphllem6  28820  oppperpex  28821  opphl  28822  outpasch  28823  hpgne1  28829  hpgne2  28830  lnopp2hpgb  28831  colopp  28837  lmieu  28852  lnperpex  28871  trgcopy  28872  trgcopyeulem  28873  acopy  28901  acopyeu  28902  inaghl  28913  leagne1  28917  leagne2  28918  leagne3  28919  leagne4  28920  cgrg3col4  28921  tgasa1  28926  f1otrg  28939  ttgbtwnid  28952  cnvbraval  32181  opsqrlem1  32211  rabfodom  32575  acunirnmpt  32732  acunirnmpt2  32733  acunirnmpt2f  32734  xrge0infss  32833  fsumiunle  32902  2exple2exp  32918  expevenpos  32919  wrdt2ind  33013  mgcf1o  33063  mndlactf1o  33090  gsummpt2d  33110  gsumwrd2dccatlem  33138  trsp2cyc  33184  cycpmrn  33204  tocyccntz  33205  cyc3evpm  33211  cyc3genpm  33213  cycpmgcl  33214  cycpmconjslem2  33216  cyc3conja  33218  archirngz  33250  archiabllem1a  33252  archiabllem1b  33253  archiabllem1  33254  archiabllem2a  33255  archiabllem2c  33256  archiabl  33259  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  elrgspnsubrun  33310  erler  33326  elrlocbasi  33327  rlocaddval  33329  rlocmulval  33330  rlocf1  33334  isdrng4  33356  fracfld  33369  imaslmod  33413  znfermltl  33426  nsgqusf1olem1  33473  lmhmqusker  33477  unitpidl1  33484  rhmquskerlem  33485  rhmimaidl  33492  drngidl  33493  isprmidlc  33507  qsidomlem2  33513  ssdifidlprm  33518  mxidlprm  33530  mxidlirredi  33531  mxidlirred  33532  drngmxidlr  33538  opprqusplusg  33549  opprqusmulr  33551  qsdrngi  33555  qsdrnglem2  33556  rprmasso2  33586  rprmirredlem  33590  1arithidom  33597  pidufd  33603  1arithufdlem1  33604  1arithufdlem2  33605  1arithufdlem3  33606  1arithufdlem4  33607  dfufd2lem  33609  dfufd2  33610  esplymhp  33712  esplyfv1  33713  esplyfv  33714  esplyfval3  33716  esplyfval1  33717  lbslelsp  33742  dimval  33745  dimvalfi  33746  lssdimle  33752  lbsdiflsp0  33770  dimkerim  33771  fedgmul  33775  dimlssid  33776  extdg1id  33810  fldextrspunlsplem  33817  extdgfialglem1  33836  extdgfialg  33838  irngnminplynz  33856  fldext2chn  33872  constrext2chnlem  33894  constrfiss  33895  constrllcllem  33896  constrlccllem  33897  constrcccllem  33898  constrcn  33904  cos9thpiminplylem2  33927  txomap  33978  qtophaus  33980  pcmplfinf  34005  zarcls1  34013  zarclsun  34014  zarclsint  34016  zarclssn  34017  zarcmplem  34025  rhmpreimacn  34029  pstmxmet  34041  pnfneige0  34095  esumcst  34207  esum2d  34237  esumiun  34238  ddemeas  34380  signsply0  34695  signstres  34719  prodfzo03  34747  actfunsnf1o  34748  actfunsnrndisj  34749  tgoldbachgt  34807  poimirlem17  37958  poimirlem20  37961  itg2gt0cn  37996  fdc1  38067  lhprelat3N  40486  dihjat2  41877  aks4d1p8  42526  primrootspoweq0  42545  aks6d1c4  42563  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  aks6d1c6lem5  42616  aks6d1c7  42623  rhmqusspan  42624  grpods  42633  unitscyglem1  42634  unitscyglem2  42635  unitscyglem3  42636  unitscyglem4  42637  aks5lem7  42639  aks5  42643  prjspersym  43040  eldioph2b  43195  diophrex  43207  irrapxlem6  43255  pellex  43263  pellfundex  43314  lnrfg  43547  mpaaeu  43578  cvgdvgrat  44740  climsuse  46038  limsupre  46069  limcleqr  46072  limsuppnfdlem  46129  liminflelimsuplem  46203  limsupub2  46240  xlimclim2lem  46267  climxlim2  46274  cncficcgt0  46316  dvbdfbdioo  46358  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem28  46456  stoweidlem29  46457  stoweidlem52  46480  stoweidlem60  46488  fourierdlem39  46574  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  hspmbllem2  47055  nnsum4primesevenALTV  48277  imaf1co  49630