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 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  xpdifid  6160  xpdifcnvepel  6161  fimaproj  8133  modmuladdnn0  13979  1arith  17019  prmgaplem5  17147  prmgapprmolem  17153  ffthiso  18020  chnso  18712  mhmid  19186  mhmmnd  19187  ghmgrp  19189  ghmqusnsg  19409  ghmquskerlem3  19413  ghmqusker  19414  ghmcmn  19958  ablfac2  20218  ringinvnz1ne0  20442  isdrng4  20902  drngidl  21448  rhmqusnsg  21488  rngqipring1  21519  isprmidlc  21535  qsidomlem2  21544  ssdifidlprm  21549  zringlpirlem1  21675  mp2pm2mplem4  23034  neiptopuni  23355  neiptoptop  23356  neiptopnei  23357  neitr  23405  hauscmplem  23631  2ndcomap  23684  lly1stc  23722  dissnref  23754  neitx  23833  cnextcn  24293  ustexsym  24442  ustex2sym  24443  ustex3sym  24444  trust  24455  utoptop  24460  restutop  24463  restutopopn  24464  ustuqtop1  24467  ustuqtop2  24468  ustuqtop3  24469  ustuqtop4  24470  utopreg  24478  ucncn  24510  fmucnd  24517  cfilufg  24518  trcfilu  24519  neipcfilu  24521  metustid  24780  metustsym  24781  metustexhalf  24782  metust  24784  cfilucfil  24785  metustbl  24792  psmetutop  24793  restmetu  24796  qdensere  24995  opnreen  25058  nmoleub2lem3  25343  ovolicc2lem4  25748  plydivlem4  26526  ulmuni  26628  dchrpt  27503  tgcgrtriv  28825  tgbtwntriv2  28829  tgbtwncom  28830  tgbtwnswapid  28834  tgbtwnintr  28835  tgbtwnouttr2  28837  tgtrisegint  28841  tgifscgr  28850  tgcgrxfr  28860  tgbtwnxfr  28872  motcgrg  28886  tgbtwnconn1lem3  28916  tgbtwnconn1  28917  tgbtwnconn3  28919  legval  28926  legov  28927  legov2  28928  legtrd  28931  legtri3  28932  legtrid  28933  ltgseg  28938  hlcgrex  28961  hlcgreulem  28962  colline  28997  tglnpt3  29001  miriso  29021  symquadlem  29040  krippenlem  29041  midexlem  29043  perpneq  29068  isperp2  29069  footexALT  29072  footex  29075  perpin  29079  perpdrag  29083  colperpexlem3  29087  colperpex  29088  opphllem  29090  mideulem  29091  midex  29092  oppne3  29098  oppnid  29101  opphllem3  29104  opphllem5  29106  opphllem6  29107  oppperpex  29108  opphl  29109  lnoppinn0  29110  outpasch  29112  hpgne1  29118  hpgne2  29119  lnopp2hpgb  29120  colopp  29126  plngrotlem1  29144  plngrotlem3  29146  lnssplnglem  29148  plng3p  29154  lmieu  29168  symquadmid  29183  lnperpex  29188  trgcopy  29190  trgcopyeulem  29191  zerocgra  29210  acopy  29220  acopyeu  29221  ragcgra  29222  perpeqlem  29226  tgaaddcpbllem1  29228  tgaaddcpbllem3  29230  tgaaddcpbl  29231  inaghl  29243  leagne1  29247  leagne2  29248  leagne3  29249  leagne4  29250  cgrg3col4  29251  cgrabasimass  29257  angmgmaddeu1  29258  angmgmaddcpbl  29269  angmgmaddcl  29270  angmgmaddlid  29271  angmgmaddrid  29272  tgasa1  29282  prlnghpg  29303  perpprlng  29307  prlngex  29308  prlngmolem1  29309  prlngmolem2  29310  prlngmid2  29318  quadcgrprlng  29323  tgaltai  29324  f1otrg  29327  ttgbtwnid  29340  cnvbraval  32591  opsqrlem1  32621  rabfodom  32980  acunirnmpt  33132  acunirnmpt2  33133  acunirnmpt2f  33134  xrge0infss  33231  fsumiunle  33299  2exple2exp  33304  expevenpos  33305  wrdt2ind  33395  mgcf1o  33443  mndlactf1o  33470  gsummpt2d  33489  gsumwrd2dccatlem  33517  trsp2cyc  33563  cycpmrn  33583  tocyccntz  33584  cyc3evpm  33590  cyc3genpm  33592  cycpmgcl  33593  cycpmconjslem2  33595  cyc3conja  33597  archirngz  33629  archiabllem1a  33631  archiabllem1b  33632  archiabllem1  33633  archiabllem2a  33634  archiabllem2c  33635  archiabl  33638  elrgspnlem1  33682  elrgspnlem2  33683  elrgspnlem4  33685  elrgspnsubrunlem1  33687  elrgspnsubrunlem2  33688  elrgspnsubrun  33689  erler  33705  elrlocbasi  33707  rlocaddval  33709  rlocmulval  33710  rlocf1  33714  rlocisunit  33716  fracfld  33749  imaslmod  33793  znfermltl  33801  nsgqusf1olem1  33842  lmhmqusker  33846  unitpidl1  33852  rhmquskerlem  33853  rhmimaidl  33860  mxidlprm  33873  mxidlirredi  33874  mxidlirred  33875  drngmxidlr  33880  opprqusplusg  33891  opprqusmulr  33893  qsdrngi  33897  qsdrnglem2  33898  dflringlem2  33905  dflring3  33907  dflring4  33908  rprmasso2  33936  rprmirredlem  33940  1arithidom  33947  pidufd  33953  1arithufdlem1  33954  1arithufdlem2  33955  1arithufdlem3  33956  1arithufdlem4  33957  dfufd2lem  33959  dfufd2  33960  esplymhp  34078  esplyfv1  34079  esplyfv  34080  esplyfval3  34082  esplyfval1  34083  lbslelsp  34108  dimval  34111  dimvalfi  34112  lssdimle  34118  lbsdiflsp0  34136  dimkerim  34137  fedgmul  34141  dimlssid  34142  extdg1id  34176  fldextrspunlsplem  34183  extdgfialglem1  34202  extdgfialg  34204  irngnminplynz  34222  fldext2chn  34238  constrext2chnlem  34260  constrfiss  34261  constrllcllem  34262  constrlccllem  34263  constrcccllem  34264  constrcn  34270  cos9thpiminplylem2  34293  txomap  34344  qtophaus  34346  pcmplfinf  34371  zarcls1  34379  zarclsun  34380  zarclsint  34382  zarclssn  34383  zarcmplem  34391  rhmpreimacn  34395  pstmxmet  34407  pnfneige0  34461  esumcst  34573  esum2d  34603  esumiun  34604  ddemeas  34747  signsply0  35059  signstres  35083  prodfzo03  35111  actfunsnf1o  35112  actfunsnrndisj  35113  tgoldbachgt  35171  poimirlem17  38386  poimirlem20  38389  itg2gt0cn  38424  fdc1  38496  lhprelat3N  40913  dihjat2  42304  aks4d1p8  42953  primrootspoweq0  42972  aks6d1c4  42990  aks6d1c6isolem1  43040  aks6d1c6isolem2  43041  aks6d1c6lem5  43043  aks6d1c7  43050  rhmqusspan  43051  grpods  43060  unitscyglem1  43061  unitscyglem2  43062  unitscyglem3  43063  unitscyglem4  43064  aks5lem7  43066  aks5  43070  prjspersym  43453  eldioph2b  43608  diophrex  43620  irrapxlem6  43668  pellex  43676  pellfundex  43727  lnrfg  43960  mpaaeu  43991  cvgdvgrat  45137  climsuse  46438  limsupre  46469  limcleqr  46472  limsuppnfdlem  46529  liminflelimsuplem  46603  limsupub2  46640  xlimclim2lem  46667  climxlim2  46674  cncficcgt0  46716  dvbdfbdioo  46758  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  stoweidlem28  46856  stoweidlem29  46857  stoweidlem52  46880  stoweidlem60  46888  fourierdlem39  46974  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem114  47048  hspmbllem2  47455  nnsum4primesevenALTV  48717  imaf1co  50081