Theorem r19.29a 3171

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

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

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 3088

This theorem is used by:  xpdifid  6159  xpdifcnvepel  6160  fimaproj  8145  modmuladdnn0  14051  1arith  17098  prmgaplem5  17226  prmgapprmolem  17232  ffthiso  18099  chnso  18791  mhmid  19266  mhmmnd  19267  ghmgrp  19269  ghmqusnsg  19489  ghmquskerlem3  19493  ghmqusker  19494  ghmcmn  20038  ablfac2  20298  ringinvnz1ne0  20524  isdrng4  20985  drngidl  21532  rhmqusnsg  21574  rngqipring1  21605  isprmidlc  21621  qsidomlem2  21630  ssdifidlprm  21635  zringlpirlem1  21761  mp2pm2mplem4  23120  neiptopuni  23441  neiptoptop  23442  neiptopnei  23443  neitr  23491  hauscmplem  23717  2ndcomap  23770  lly1stc  23808  dissnref  23840  neitx  23919  cnextcn  24379  ustexsym  24528  ustex2sym  24529  ustex3sym  24530  trust  24541  utoptop  24546  restutop  24549  restutopopn  24550  ustuqtop1  24553  ustuqtop2  24554  ustuqtop3  24555  ustuqtop4  24556  utopreg  24564  ucncn  24596  fmucnd  24603  cfilufg  24604  trcfilu  24605  neipcfilu  24607  metustid  24866  metustsym  24867  metustexhalf  24868  metust  24870  cfilucfil  24871  metustbl  24878  psmetutop  24879  restmetu  24882  qdensere  25081  opnreen  25144  nmoleub2lem3  25429  ovolicc2lem4  25834  plydivlem4  26610  ulmuni  26712  dchrpt  27587  tgcgrtriv  28939  tgbtwntriv2  28943  tgbtwncom  28944  tgbtwnswapid  28948  tgbtwnintr  28949  tgbtwnouttr2  28951  tgtrisegint  28955  tgifscgr  28964  tgcgrxfr  28974  tgbtwnxfr  28986  motcgrg  29000  tgbtwnconn1lem3  29030  tgbtwnconn1  29031  tgbtwnconn3  29033  legval  29040  legov  29041  legov2  29042  legtrd  29045  legtri3  29046  legtrid  29047  ltgseg  29052  hlcgrex  29075  hlcgreulem  29076  colline  29111  tglnpt3  29115  miriso  29135  symquadlem  29154  krippenlem  29155  midexlem  29157  perpneq  29182  isperp2  29183  footexALT  29186  footex  29189  perpin  29193  perpdrag  29197  colperpexlem3  29201  colperpex  29202  opphllem  29204  mideulem  29205  midex  29206  oppne3  29212  oppnid  29215  opphllem3  29218  opphllem5  29220  opphllem6  29221  oppperpex  29222  opphl  29223  lnoppinn0  29224  outpasch  29226  hpgne1  29232  hpgne2  29233  lnopp2hpgb  29234  colopp  29240  plngrotlem1  29258  plngrotlem3  29260  lnssplnglem  29262  plng3p  29268  lmieu  29282  symquadmid  29297  lnperpex  29302  trgcopy  29304  trgcopyeulem  29305  zerocgra  29324  acopy  29334  acopyeu  29335  ragcgra  29336  perpeqlem  29340  tgaaddcpbllem1  29342  tgaaddcpbllem3  29344  tgaaddcpbl  29345  inaghl  29357  leagne1  29361  leagne2  29362  leagne3  29363  leagne4  29364  cgrg3col4  29365  cgrabasimass  29371  angmgmaddeu1  29372  angmgmaddcpbl  29383  angmgmaddcl  29384  angmgmaddlid  29385  angmgmaddrid  29386  tgasa1  29396  prlnghpg  29417  perpprlng  29421  prlngex  29422  prlngmolem1  29423  prlngmolem2  29424  prlngmid2  29432  quadcgrprlng  29437  tgaltai  29438  f1otrg  29441  ttgbtwnid  29454  cnvbraval  32705  opsqrlem1  32735  rabfodom  33094  acunirnmpt  33246  acunirnmpt2  33247  acunirnmpt2f  33248  xrge0infss  33345  fsumiunle  33413  2exple2exp  33418  expevenpos  33419  wrdt2ind  33509  mgcf1o  33557  mndlactf1o  33584  gsummpt2d  33603  gsumwrd2dccatlem  33631  trsp2cyc  33677  cycpmrn  33697  tocyccntz  33698  cyc3evpm  33704  cyc3genpm  33706  cycpmgcl  33707  cycpmconjslem2  33709  cyc3conja  33711  archirngz  33743  archiabllem1a  33745  archiabllem1b  33746  archiabllem1  33747  archiabllem2a  33748  archiabllem2c  33749  archiabl  33752  elrgspnlem1  33796  elrgspnlem2  33797  elrgspnlem4  33799  elrgspnsubrunlem1  33801  elrgspnsubrunlem2  33802  elrgspnsubrun  33803  erler  33819  elrlocbasi  33821  rlocaddval  33823  rlocmulval  33824  rlocf1  33828  rlocisunit  33830  fracfld  33863  imaslmod  33907  znfermltl  33915  nsgqusf1olem1  33957  lmhmqusker  33961  unitpidl1  33967  rhmquskerlem  33968  rhmimaidl  33975  mxidlprm  33988  mxidlirredi  33989  mxidlirred  33990  drngmxidlr  33995  opprqusplusg  34006  opprqusmulr  34008  qsdrngi  34012  qsdrnglem2  34013  dflringlem2  34020  dflring3  34022  dflring4  34023  rprmasso2  34051  rprmirredlem  34055  1arithidom  34062  pidufd  34068  1arithufdlem1  34069  1arithufdlem2  34070  1arithufdlem3  34071  1arithufdlem4  34072  dfufd2lem  34074  dfufd2  34075  esplymhp  34193  esplyfv1  34194  esplyfv  34195  esplyfval3  34197  esplyfval1  34198  lbslelsp  34223  dimval  34226  dimvalfi  34227  lssdimle  34233  lbsdiflsp0  34251  dimkerim  34252  fedgmul  34256  dimlssid  34257  extdg1id  34291  fldextrspunlsplem  34298  extdgfialglem1  34317  extdgfialg  34319  irngnminplynz  34337  fldext2chn  34353  constrext2chnlem  34375  constrfiss  34376  constrllcllem  34377  constrlccllem  34378  constrcccllem  34379  constrcn  34385  cos9thpiminplylem2  34408  txomap  34459  qtophaus  34461  pcmplfinf  34486  zarcls1  34494  zarclsun  34495  zarclsint  34497  zarclssn  34498  zarcmplem  34506  rhmpreimacn  34510  pstmxmet  34522  pnfneige0  34576  esumcst  34688  esum2d  34718  esumiun  34719  ddemeas  34862  signsply0  35173  signstres  35197  prodfzo03  35225  actfunsnf1o  35226  actfunsnrndisj  35227  tgoldbachgt  35285  poimirlem17  38535  poimirlem20  38538  itg2gt0cn  38573  fdc1  38660  lhprelat3N  41077  dihjat2  42468  aks4d1p8  43117  primrootspoweq0  43136  aks6d1c4  43154  aks6d1c6isolem1  43204  aks6d1c6isolem2  43205  aks6d1c6lem5  43207  aks6d1c7  43214  rhmqusspan  43215  grpods  43224  unitscyglem1  43225  unitscyglem2  43226  unitscyglem3  43227  unitscyglem4  43228  aks5lem7  43230  aks5  43234  prjspersym  43615  eldioph2b  43753  diophrex  43765  irrapxlem6  43813  pellex  43821  pellfundex  43872  lnrfg  44105  mpaaeu  44136  cvgdvgrat  45282  climsuse  46589  limsupre  46620  limcleqr  46623  limsuppnfdlem  46680  liminflelimsuplem  46754  limsupub2  46791  xlimclim2lem  46818  climxlim2  46825  cncficcgt0  46867  dvbdfbdioo  46909  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  stoweidlem28  47007  stoweidlem29  47008  stoweidlem52  47031  stoweidlem60  47039  fourierdlem39  47125  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem114  47199  hspmbllem2  47606  nnsum4primesevenALTV  48868  imaf1co  50232