Theorem r19.29a 3174

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

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

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 1945

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

This theorem is used by:  xpdifid  6175  xpdifcnvepel  6176  fimaproj  8187  modmuladdnn0  14096  1arith  17146  prmgaplem5  17274  prmgapprmolem  17280  ffthiso  18147  chnso  18839  mhmid  19314  mhmmnd  19315  ghmgrp  19317  ghmqusnsg  19538  ghmquskerlem3  19542  ghmqusker  19543  ghmcmn  20087  ablfac2  20347  ringinvnz1ne0  20573  isdrng4  21034  drngidl  21581  rhmqusnsg  21623  rngqipring1  21654  isprmidlc  21670  qsidomlem2  21679  ssdifidlprm  21684  zringlpirlem1  21812  mp2pm2mplem4  23171  neiptopuni  23492  neiptoptop  23493  neiptopnei  23494  neitr  23542  hauscmplem  23768  2ndcomap  23821  lly1stc  23859  dissnref  23891  neitx  23970  cnextcn  24430  ustexsym  24579  ustex2sym  24580  ustex3sym  24581  trust  24592  utoptop  24597  restutop  24600  restutopopn  24601  ustuqtop1  24604  ustuqtop2  24605  ustuqtop3  24606  ustuqtop4  24607  utopreg  24615  ucncn  24647  fmucnd  24654  cfilufg  24655  trcfilu  24656  neipcfilu  24658  metustid  24917  metustsym  24918  metustexhalf  24919  metust  24921  cfilucfil  24922  metustbl  24929  psmetutop  24930  restmetu  24933  qdensere  25132  opnreen  25195  nmoleub2lem3  25480  ovolicc2lem4  25885  plydivlem4  26661  ulmuni  26765  dchrpt  27640  tgcgrtriv  28992  tgbtwntriv2  28996  tgbtwncom  28997  tgbtwnswapid  29001  tgbtwnintr  29002  tgbtwnouttr2  29004  tgtrisegint  29008  tgifscgr  29017  tgcgrxfr  29027  tgbtwnxfr  29039  motcgrg  29053  tgbtwnconn1lem3  29083  tgbtwnconn1  29084  tgbtwnconn3  29086  legval  29093  legov  29094  legov2  29095  legtrd  29098  legtri3  29099  legtrid  29100  ltgseg  29105  hlcgrex  29128  hlcgreulem  29129  colline  29164  tglnpt3  29168  miriso  29188  symquadlem  29207  krippenlem  29208  midexlem  29210  perpneq  29235  isperp2  29236  footexALT  29239  footex  29242  perpin  29246  perpdrag  29250  colperpexlem3  29254  colperpex  29255  opphllem  29257  mideulem  29258  midex  29259  oppne3  29265  oppnid  29268  opphllem3  29271  opphllem5  29273  opphllem6  29274  oppperpex  29275  opphl  29276  lnoppinn0  29277  outpasch  29279  hpgne1  29285  hpgne2  29286  lnopp2hpgb  29287  colopp  29293  plngrotlem1  29311  plngrotlem3  29313  lnssplnglem  29315  plng3p  29321  lmieu  29335  symquadmid  29350  lnperpex  29355  trgcopy  29357  trgcopyeulem  29358  zerocgra  29377  acopy  29387  acopyeu  29388  ragcgra  29389  perpeqlem  29393  tgaaddcpbllem1  29395  tgaaddcpbllem3  29397  tgaaddcpbl  29398  inaghl  29410  leagne1  29414  leagne2  29415  leagne3  29416  leagne4  29417  cgrg3col4  29418  cgrabasimass  29424  angmgmaddeu1  29425  angmgmaddcpbl  29436  angmgmaddcl  29437  angmgmaddlid  29438  angmgmaddrid  29439  tgasa1  29449  prlnghpg  29470  perpprlng  29474  prlngex  29475  prlngmolem1  29476  prlngmolem2  29477  prlngmid2  29485  quadcgrprlng  29490  tgaltai  29491  f1otrg  29494  ttgbtwnid  29507  cnvbraval  32758  opsqrlem1  32788  inagbtwn  33094  inagcgrabtwn  33097  leacgra2  33108  leacgra1  33109  tgextalem1inag  33116  tgexta  33124  tgaas1  33131  rabfodom  33189  acunirnmpt  33341  acunirnmpt2  33342  acunirnmpt2f  33343  xrge0infss  33438  fsumiunle  33506  2exple2exp  33511  expevenpos  33512  wrdt2ind  33602  weinfcl  33626  mgcf1o  33653  mndlactf1o  33680  gsummpt2d  33699  gsumwrd2dccatlem  33727  trsp2cyc  33773  cycpmrn  33793  tocyccntz  33794  cyc3evpm  33800  cyc3genpm  33802  cycpmgcl  33803  cycpmconjslem2  33805  cyc3conja  33807  archirngz  33839  archiabllem1a  33841  archiabllem1b  33842  archiabllem1  33843  archiabllem2a  33844  archiabllem2c  33845  archiabl  33848  elrgspnlem1  33892  elrgspnlem2  33893  elrgspnlem4  33895  elrgspnsubrunlem1  33897  elrgspnsubrunlem2  33898  elrgspnsubrun  33899  erler  33915  elrlocbasi  33917  rlocaddval  33919  rlocmulval  33920  rlocf1  33924  rlocisunit  33926  fracfld  33967  imaslmod  34011  znfermltl  34019  nsgqusf1olem1  34061  lmhmqusker  34065  unitpidl1  34071  rhmquskerlem  34072  rhmimaidl  34079  mxidlprm  34092  mxidlirredi  34093  mxidlirred  34094  drngmxidlr  34099  opprqusplusg  34110  opprqusmulr  34112  qsdrngi  34116  qsdrnglem2  34117  dflringlem2  34124  dflring3  34126  dflring4  34127  rprmasso2  34155  rprmirredlem  34159  1arithidom  34166  pidufd  34172  1arithufdlem1  34173  1arithufdlem2  34174  1arithufdlem3  34175  1arithufdlem4  34176  dfufd2lem  34178  dfufd2  34179  rngunsnply1chr2  34246  esplymhp  34304  esplyfv1  34305  esplyfv  34306  esplyfval3  34308  esplyfval1  34309  lbslelsp  34334  dimval  34337  dimvalfi  34338  lssdimle  34344  lbsdiflsp0  34362  dimkerim  34363  fedgmul  34367  dimlssid  34368  extdg1id  34402  fldextrspunlsplem  34409  extdgfialglem1  34428  extdgfialg  34430  irngnminplynz  34448  fldext2chn  34464  constrext2chnlem  34486  constrfiss  34487  constrllcllem  34488  constrlccllem  34489  constrcccllem  34490  constrcn  34496  cos9thpiminplylem2  34519  txomap  34570  qtophaus  34572  pcmplfinf  34597  zarcls1  34605  zarclsun  34606  zarclsint  34608  zarclssn  34609  zarcmplem  34617  rhmpreimacn  34621  pstmxmet  34633  pnfneige0  34687  esumcst  34799  esum2d  34829  esumiun  34830  ddemeas  34973  signsply0  35284  signstres  35308  prodfzo03  35336  actfunsnf1o  35337  actfunsnrndisj  35338  tgoldbachgt  35396  poimirlem17  38816  poimirlem20  38819  itg2gt0cn  38854  fdc1  38939  lhprelat3N  41356  dihjat2  42747  aks4d1p8  43396  primrootspoweq0  43415  aks6d1c4  43433  aks6d1c6isolem1  43483  aks6d1c6isolem2  43484  aks6d1c6lem5  43486  aks6d1c7  43493  rhmqusspan  43494  grpods  43503  unitscyglem1  43504  unitscyglem2  43505  unitscyglem3  43506  unitscyglem4  43507  aks5lem7  43509  aks5  43513  prjspersym  43895  eldioph2b  44034  diophrex  44046  irrapxlem6  44094  pellex  44102  pellfundex  44153  lnrfg  44380  mpaaeu  44411  cvgdvgrat  45552  climsuse  46887  limsupre  46918  limcleqr  46921  limsuppnfdlem  46978  liminflelimsuplem  47052  limsupub2  47089  xlimclim2lem  47116  climxlim2  47123  cncficcgt0  47165  dvbdfbdioo  47207  ioodvbdlimc1lem2  47209  ioodvbdlimc2lem  47211  stoweidlem28  47305  stoweidlem29  47306  stoweidlem52  47329  stoweidlem60  47337  fourierdlem39  47423  fourierdlem102  47485  fourierdlem103  47486  fourierdlem104  47487  fourierdlem114  47497  hspmbllem2  47904  nnsum4primesevenALTV  49166  imaf1co  50596