Theorem r19.29a 3170

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  xpdifid  6158  xpdifcnvepel  6159  fimaproj  8155  modmuladdnn0  14062  1arith  17111  prmgaplem5  17239  prmgapprmolem  17245  ffthiso  18112  chnso  18804  mhmid  19279  mhmmnd  19280  ghmgrp  19282  ghmqusnsg  19502  ghmquskerlem3  19506  ghmqusker  19507  ghmcmn  20051  ablfac2  20311  ringinvnz1ne0  20537  isdrng4  20998  drngidl  21545  rhmqusnsg  21587  rngqipring1  21618  isprmidlc  21634  qsidomlem2  21643  ssdifidlprm  21648  zringlpirlem1  21774  mp2pm2mplem4  23133  neiptopuni  23454  neiptoptop  23455  neiptopnei  23456  neitr  23504  hauscmplem  23730  2ndcomap  23783  lly1stc  23821  dissnref  23853  neitx  23932  cnextcn  24392  ustexsym  24541  ustex2sym  24542  ustex3sym  24543  trust  24554  utoptop  24559  restutop  24562  restutopopn  24563  ustuqtop1  24566  ustuqtop2  24567  ustuqtop3  24568  ustuqtop4  24569  utopreg  24577  ucncn  24609  fmucnd  24616  cfilufg  24617  trcfilu  24618  neipcfilu  24620  metustid  24879  metustsym  24880  metustexhalf  24881  metust  24883  cfilucfil  24884  metustbl  24891  psmetutop  24892  restmetu  24895  qdensere  25094  opnreen  25157  nmoleub2lem3  25442  ovolicc2lem4  25847  plydivlem4  26623  ulmuni  26725  dchrpt  27600  tgcgrtriv  28952  tgbtwntriv2  28956  tgbtwncom  28957  tgbtwnswapid  28961  tgbtwnintr  28962  tgbtwnouttr2  28964  tgtrisegint  28968  tgifscgr  28977  tgcgrxfr  28987  tgbtwnxfr  28999  motcgrg  29013  tgbtwnconn1lem3  29043  tgbtwnconn1  29044  tgbtwnconn3  29046  legval  29053  legov  29054  legov2  29055  legtrd  29058  legtri3  29059  legtrid  29060  ltgseg  29065  hlcgrex  29088  hlcgreulem  29089  colline  29124  tglnpt3  29128  miriso  29148  symquadlem  29167  krippenlem  29168  midexlem  29170  perpneq  29195  isperp2  29196  footexALT  29199  footex  29202  perpin  29206  perpdrag  29210  colperpexlem3  29214  colperpex  29215  opphllem  29217  mideulem  29218  midex  29219  oppne3  29225  oppnid  29228  opphllem3  29231  opphllem5  29233  opphllem6  29234  oppperpex  29235  opphl  29236  lnoppinn0  29237  outpasch  29239  hpgne1  29245  hpgne2  29246  lnopp2hpgb  29247  colopp  29253  plngrotlem1  29271  plngrotlem3  29273  lnssplnglem  29275  plng3p  29281  lmieu  29295  symquadmid  29310  lnperpex  29315  trgcopy  29317  trgcopyeulem  29318  zerocgra  29337  acopy  29347  acopyeu  29348  ragcgra  29349  perpeqlem  29353  tgaaddcpbllem1  29355  tgaaddcpbllem3  29357  tgaaddcpbl  29358  inaghl  29370  leagne1  29374  leagne2  29375  leagne3  29376  leagne4  29377  cgrg3col4  29378  cgrabasimass  29384  angmgmaddeu1  29385  angmgmaddcpbl  29396  angmgmaddcl  29397  angmgmaddlid  29398  angmgmaddrid  29399  tgasa1  29409  prlnghpg  29430  perpprlng  29434  prlngex  29435  prlngmolem1  29436  prlngmolem2  29437  prlngmid2  29445  quadcgrprlng  29450  tgaltai  29451  f1otrg  29454  ttgbtwnid  29467  cnvbraval  32718  opsqrlem1  32748  inagbtwn  33054  inagcgrabtwn  33057  leacgra2  33068  leacgra1  33069  tgextalem1inag  33076  tgexta  33084  tgaas1  33091  rabfodom  33149  acunirnmpt  33301  acunirnmpt2  33302  acunirnmpt2f  33303  xrge0infss  33399  fsumiunle  33467  2exple2exp  33472  expevenpos  33473  wrdt2ind  33563  mgcf1o  33611  mndlactf1o  33638  gsummpt2d  33657  gsumwrd2dccatlem  33685  trsp2cyc  33731  cycpmrn  33751  tocyccntz  33752  cyc3evpm  33758  cyc3genpm  33760  cycpmgcl  33761  cycpmconjslem2  33763  cyc3conja  33765  archirngz  33797  archiabllem1a  33799  archiabllem1b  33800  archiabllem1  33801  archiabllem2a  33802  archiabllem2c  33803  archiabl  33806  elrgspnlem1  33850  elrgspnlem2  33851  elrgspnlem4  33853  elrgspnsubrunlem1  33855  elrgspnsubrunlem2  33856  elrgspnsubrun  33857  erler  33873  elrlocbasi  33875  rlocaddval  33877  rlocmulval  33878  rlocf1  33882  rlocisunit  33884  fracfld  33917  imaslmod  33961  znfermltl  33969  nsgqusf1olem1  34011  lmhmqusker  34015  unitpidl1  34021  rhmquskerlem  34022  rhmimaidl  34029  mxidlprm  34042  mxidlirredi  34043  mxidlirred  34044  drngmxidlr  34049  opprqusplusg  34060  opprqusmulr  34062  qsdrngi  34066  qsdrnglem2  34067  dflringlem2  34074  dflring3  34076  dflring4  34077  rprmasso2  34105  rprmirredlem  34109  1arithidom  34116  pidufd  34122  1arithufdlem1  34123  1arithufdlem2  34124  1arithufdlem3  34125  1arithufdlem4  34126  dfufd2lem  34128  dfufd2  34129  esplymhp  34247  esplyfv1  34248  esplyfv  34249  esplyfval3  34251  esplyfval1  34252  lbslelsp  34277  dimval  34280  dimvalfi  34281  lssdimle  34287  lbsdiflsp0  34305  dimkerim  34306  fedgmul  34310  dimlssid  34311  extdg1id  34345  fldextrspunlsplem  34352  extdgfialglem1  34371  extdgfialg  34373  irngnminplynz  34391  fldext2chn  34407  constrext2chnlem  34429  constrfiss  34430  constrllcllem  34431  constrlccllem  34432  constrcccllem  34433  constrcn  34439  cos9thpiminplylem2  34462  txomap  34513  qtophaus  34515  pcmplfinf  34540  zarcls1  34548  zarclsun  34549  zarclsint  34551  zarclssn  34552  zarcmplem  34560  rhmpreimacn  34564  pstmxmet  34576  pnfneige0  34630  esumcst  34742  esum2d  34772  esumiun  34773  ddemeas  34916  signsply0  35227  signstres  35251  prodfzo03  35279  actfunsnf1o  35280  actfunsnrndisj  35281  tgoldbachgt  35339  poimirlem17  38649  poimirlem20  38652  itg2gt0cn  38687  fdc1  38774  lhprelat3N  41191  dihjat2  42582  aks4d1p8  43231  primrootspoweq0  43250  aks6d1c4  43268  aks6d1c6isolem1  43318  aks6d1c6isolem2  43319  aks6d1c6lem5  43321  aks6d1c7  43328  rhmqusspan  43329  grpods  43338  unitscyglem1  43339  unitscyglem2  43340  unitscyglem3  43341  unitscyglem4  43342  aks5lem7  43344  aks5  43348  prjspersym  43729  eldioph2b  43868  diophrex  43880  irrapxlem6  43928  pellex  43936  pellfundex  43987  lnrfg  44215  mpaaeu  44246  cvgdvgrat  45391  climsuse  46714  limsupre  46745  limcleqr  46748  limsuppnfdlem  46805  liminflelimsuplem  46879  limsupub2  46916  xlimclim2lem  46943  climxlim2  46950  cncficcgt0  46992  dvbdfbdioo  47034  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  stoweidlem28  47132  stoweidlem29  47133  stoweidlem52  47156  stoweidlem60  47164  fourierdlem39  47250  fourierdlem102  47312  fourierdlem103  47313  fourierdlem104  47314  fourierdlem114  47324  hspmbllem2  47731  nnsum4primesevenALTV  48993  imaf1co  50365