Theorem r19.29a 3137

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  xpdifid  6121  fimaproj  8075  modmuladdnn0  13840  1arith  16857  prmgaplem5  16985  prmgapprmolem  16991  ffthiso  17856  mhmid  18960  mhmmnd  18961  ghmgrp  18963  ghmqusnsg  19179  ghmquskerlem3  19183  ghmqusker  19184  ghmcmn  19728  ablfac2  19988  ringinvnz1ne0  20203  rhmqusnsg  21210  rngqipring1  21241  zringlpirlem1  21387  mp2pm2mplem4  22712  neiptopuni  23033  neiptoptop  23034  neiptopnei  23035  neitr  23083  hauscmplem  23309  2ndcomap  23361  lly1stc  23399  dissnref  23431  neitx  23510  cnextcn  23970  ustexsym  24119  ustex2sym  24120  ustex3sym  24121  trust  24133  utoptop  24138  restutop  24141  restutopopn  24142  ustuqtop1  24145  ustuqtop2  24146  ustuqtop3  24147  ustuqtop4  24148  utopreg  24156  ucncn  24188  fmucnd  24195  cfilufg  24196  trcfilu  24197  neipcfilu  24199  metustid  24458  metustsym  24459  metustexhalf  24460  metust  24462  cfilucfil  24463  metustbl  24470  psmetutop  24471  restmetu  24474  qdensere  24673  opnreen  24736  nmoleub2lem3  25031  ovolicc2lem4  25437  plydivlem4  26220  ulmuni  26317  dchrpt  27194  tgcgrtriv  28447  tgbtwntriv2  28450  tgbtwncom  28451  tgbtwnswapid  28455  tgbtwnintr  28456  tgbtwnouttr2  28458  tgtrisegint  28462  tgifscgr  28471  tgcgrxfr  28481  tgbtwnxfr  28493  motcgrg  28507  tgbtwnconn1lem3  28537  tgbtwnconn1  28538  tgbtwnconn3  28540  legval  28547  legov  28548  legov2  28549  legtrd  28552  legtri3  28553  legtrid  28554  ltgseg  28559  hlcgrex  28579  hlcgreulem  28580  colline  28612  miriso  28633  symquadlem  28652  krippenlem  28653  midexlem  28655  perpneq  28677  isperp2  28678  footexALT  28681  footex  28684  perpdrag  28691  colperpexlem3  28695  colperpex  28696  opphllem  28698  mideulem  28699  midex  28700  oppne3  28706  oppnid  28709  opphllem3  28712  opphllem5  28714  opphllem6  28715  oppperpex  28716  opphl  28717  outpasch  28718  hpgne1  28724  hpgne2  28725  lnopp2hpgb  28726  colopp  28732  lmieu  28747  lnperpex  28766  trgcopy  28767  trgcopyeulem  28768  acopy  28796  acopyeu  28797  inaghl  28808  leagne1  28812  leagne2  28813  leagne3  28814  leagne4  28815  cgrg3col4  28816  tgasa1  28821  f1otrg  28834  ttgbtwnid  28847  cnvbraval  32072  opsqrlem1  32102  rabfodom  32467  acunirnmpt  32616  acunirnmpt2  32617  acunirnmpt2f  32618  xrge0infss  32716  fsumiunle  32787  2exple2exp  32803  expevenpos  32804  wrdt2ind  32908  mgcf1o  32958  chnso  32969  mndlactf1o  32997  gsummpt2d  33015  gsumwrd2dccatlem  33032  trsp2cyc  33078  cycpmrn  33098  tocyccntz  33099  cyc3evpm  33105  cyc3genpm  33107  cycpmgcl  33108  cycpmconjslem2  33110  cyc3conja  33112  archirngz  33144  archiabllem1a  33146  archiabllem1b  33147  archiabllem1  33148  archiabllem2a  33149  archiabllem2c  33150  archiabl  33153  elrgspnlem1  33195  elrgspnlem2  33196  elrgspnlem4  33198  elrgspnsubrunlem1  33200  elrgspnsubrunlem2  33201  elrgspnsubrun  33202  erler  33218  elrlocbasi  33219  rlocaddval  33221  rlocmulval  33222  rlocf1  33226  isdrng4  33247  fracfld  33260  imaslmod  33303  znfermltl  33316  nsgqusf1olem1  33363  lmhmqusker  33367  unitpidl1  33374  rhmquskerlem  33375  rhmimaidl  33382  drngidl  33383  isprmidlc  33397  qsidomlem2  33403  ssdifidlprm  33408  mxidlprm  33420  mxidlirredi  33421  mxidlirred  33422  drngmxidlr  33428  opprqusplusg  33439  opprqusmulr  33441  qsdrngi  33445  qsdrnglem2  33446  rprmasso2  33476  rprmirredlem  33480  1arithidom  33487  pidufd  33493  1arithufdlem1  33494  1arithufdlem2  33495  1arithufdlem3  33496  1arithufdlem4  33497  dfufd2lem  33499  dfufd2  33500  lbslelsp  33572  dimval  33575  dimvalfi  33576  lssdimle  33582  lbsdiflsp0  33601  dimkerim  33602  fedgmul  33606  dimlssid  33607  extdg1id  33640  fldextrspunlsplem  33647  irngnminplynz  33681  fldext2chn  33697  constrext2chnlem  33719  constrfiss  33720  constrllcllem  33721  constrlccllem  33722  constrcccllem  33723  constrcn  33729  cos9thpiminplylem2  33752  txomap  33803  qtophaus  33805  pcmplfinf  33830  zarcls1  33838  zarclsun  33839  zarclsint  33841  zarclssn  33842  zarcmplem  33850  rhmpreimacn  33854  pstmxmet  33866  pnfneige0  33920  esumcst  34032  esum2d  34062  esumiun  34063  ddemeas  34205  signsply0  34521  signstres  34545  prodfzo03  34573  actfunsnf1o  34574  actfunsnrndisj  34575  tgoldbachgt  34633  poimirlem17  37619  poimirlem20  37622  itg2gt0cn  37657  fdc1  37728  lhprelat3N  40022  dihjat2  41413  aks4d1p8  42063  primrootspoweq0  42082  aks6d1c4  42100  aks6d1c6isolem1  42150  aks6d1c6isolem2  42151  aks6d1c6lem5  42153  aks6d1c7  42160  rhmqusspan  42161  grpods  42170  unitscyglem1  42171  unitscyglem2  42172  unitscyglem3  42173  unitscyglem4  42174  aks5lem7  42176  aks5  42180  prjspersym  42583  eldioph2b  42739  diophrex  42751  irrapxlem6  42803  pellex  42811  pellfundex  42862  lnrfg  43095  mpaaeu  43126  cvgdvgrat  44289  climsuse  45593  limsupre  45626  limcleqr  45629  limsuppnfdlem  45686  liminflelimsuplem  45760  limsupub2  45797  xlimclim2lem  45824  climxlim2  45831  cncficcgt0  45873  dvbdfbdioo  45915  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  stoweidlem28  46013  stoweidlem29  46014  stoweidlem52  46037  stoweidlem60  46045  fourierdlem39  46131  fourierdlem102  46193  fourierdlem103  46194  fourierdlem104  46195  fourierdlem114  46205  hspmbllem2  46612  nnsum4primesevenALTV  47789  imaf1co  49144