Theorem r19.29a 3175

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

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

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 3092

This theorem is used by:  xpdifid  6167  xpdifcnvepel  6168  fimaproj  8133  modmuladdnn0  13964  1arith  17004  prmgaplem5  17132  prmgapprmolem  17138  ffthiso  18005  chnso  18697  mhmid  19152  mhmmnd  19153  ghmgrp  19155  ghmqusnsg  19375  ghmquskerlem3  19379  ghmqusker  19380  ghmcmn  19924  ablfac2  20184  ringinvnz1ne0  20408  isdrng4  20868  drngidl  21414  rhmqusnsg  21454  rngqipring1  21485  isprmidlc  21501  qsidomlem2  21510  ssdifidlprm  21515  zringlpirlem1  21641  mp2pm2mplem4  22995  neiptopuni  23316  neiptoptop  23317  neiptopnei  23318  neitr  23366  hauscmplem  23592  2ndcomap  23644  lly1stc  23682  dissnref  23714  neitx  23793  cnextcn  24253  ustexsym  24402  ustex2sym  24403  ustex3sym  24404  trust  24415  utoptop  24420  restutop  24423  restutopopn  24424  ustuqtop1  24427  ustuqtop2  24428  ustuqtop3  24429  ustuqtop4  24430  utopreg  24438  ucncn  24470  fmucnd  24477  cfilufg  24478  trcfilu  24479  neipcfilu  24481  metustid  24740  metustsym  24741  metustexhalf  24742  metust  24744  cfilucfil  24745  metustbl  24752  psmetutop  24753  restmetu  24756  qdensere  24955  opnreen  25018  nmoleub2lem3  25303  ovolicc2lem4  25708  plydivlem4  26486  ulmuni  26584  dchrpt  27460  tgcgrtriv  28782  tgbtwntriv2  28785  tgbtwncom  28786  tgbtwnswapid  28790  tgbtwnintr  28791  tgbtwnouttr2  28793  tgtrisegint  28797  tgifscgr  28806  tgcgrxfr  28816  tgbtwnxfr  28828  motcgrg  28842  tgbtwnconn1lem3  28872  tgbtwnconn1  28873  tgbtwnconn3  28875  legval  28882  legov  28883  legov2  28884  legtrd  28887  legtri3  28888  legtrid  28889  ltgseg  28894  hlcgrex  28917  hlcgreulem  28918  colline  28952  tglnpt3  28956  miriso  28976  symquadlem  28995  krippenlem  28996  midexlem  28998  perpneq  29023  isperp2  29024  footexALT  29027  footex  29030  perpin  29034  perpdrag  29038  colperpexlem3  29042  colperpex  29043  opphllem  29045  mideulem  29046  midex  29047  oppne3  29053  oppnid  29056  opphllem3  29059  opphllem5  29061  opphllem6  29062  oppperpex  29063  opphl  29064  outpasch  29066  hpgne1  29072  hpgne2  29073  lnopp2hpgb  29074  colopp  29080  plngrotlem1  29098  plngrotlem3  29100  lnssplnglem  29102  plng3p  29108  lmieu  29122  symquadmid  29137  lnperpex  29142  trgcopy  29144  trgcopyeulem  29145  acopy  29173  acopyeu  29174  ragcgra  29175  perpeqlem  29179  inaghl  29191  leagne1  29195  leagne2  29196  leagne3  29197  leagne4  29198  cgrg3col4  29199  tgasa1  29204  prlnghpg  29225  perpprlng  29229  prlngex  29230  prlngmolem1  29231  prlngmolem2  29232  prlngmid2  29240  quadcgrprlng  29245  tgaltai  29246  f1otrg  29249  ttgbtwnid  29262  cnvbraval  32491  opsqrlem1  32521  rabfodom  32880  acunirnmpt  33033  acunirnmpt2  33034  acunirnmpt2f  33035  xrge0infss  33134  fsumiunle  33202  2exple2exp  33207  expevenpos  33208  wrdt2ind  33298  mgcf1o  33346  mndlactf1o  33373  gsummpt2d  33392  gsumwrd2dccatlem  33420  trsp2cyc  33466  cycpmrn  33486  tocyccntz  33487  cyc3evpm  33493  cyc3genpm  33495  cycpmgcl  33496  cycpmconjslem2  33498  cyc3conja  33500  archirngz  33532  archiabllem1a  33534  archiabllem1b  33535  archiabllem1  33536  archiabllem2a  33537  archiabllem2c  33538  archiabl  33541  elrgspnlem1  33585  elrgspnlem2  33586  elrgspnlem4  33588  elrgspnsubrunlem1  33590  elrgspnsubrunlem2  33591  elrgspnsubrun  33592  erler  33608  elrlocbasi  33610  rlocaddval  33612  rlocmulval  33613  rlocf1  33617  rlocisunit  33619  fracfld  33652  imaslmod  33696  znfermltl  33704  nsgqusf1olem1  33745  lmhmqusker  33749  unitpidl1  33755  rhmquskerlem  33756  rhmimaidl  33763  mxidlprm  33776  mxidlirredi  33777  mxidlirred  33778  drngmxidlr  33783  opprqusplusg  33794  opprqusmulr  33796  qsdrngi  33800  qsdrnglem2  33801  dflringlem2  33808  dflring3  33810  dflring4  33811  rprmasso2  33839  rprmirredlem  33843  1arithidom  33850  pidufd  33856  1arithufdlem1  33857  1arithufdlem2  33858  1arithufdlem3  33859  1arithufdlem4  33860  dfufd2lem  33862  dfufd2  33863  esplymhp  33981  esplyfv1  33982  esplyfv  33983  esplyfval3  33985  esplyfval1  33986  lbslelsp  34011  dimval  34014  dimvalfi  34015  lssdimle  34021  lbsdiflsp0  34039  dimkerim  34040  fedgmul  34044  dimlssid  34045  extdg1id  34079  fldextrspunlsplem  34086  extdgfialglem1  34105  extdgfialg  34107  irngnminplynz  34125  fldext2chn  34141  constrext2chnlem  34163  constrfiss  34164  constrllcllem  34165  constrlccllem  34166  constrcccllem  34167  constrcn  34173  cos9thpiminplylem2  34196  txomap  34247  qtophaus  34249  pcmplfinf  34274  zarcls1  34282  zarclsun  34283  zarclsint  34285  zarclssn  34286  zarcmplem  34294  rhmpreimacn  34298  pstmxmet  34310  pnfneige0  34364  esumcst  34476  esum2d  34506  esumiun  34507  ddemeas  34650  signsply0  34962  signstres  34986  prodfzo03  35014  actfunsnf1o  35015  actfunsnrndisj  35016  tgoldbachgt  35074  poimirlem17  38321  poimirlem20  38324  itg2gt0cn  38359  fdc1  38430  lhprelat3N  40847  dihjat2  42238  aks4d1p8  42887  primrootspoweq0  42906  aks6d1c4  42924  aks6d1c6isolem1  42974  aks6d1c6isolem2  42975  aks6d1c6lem5  42977  aks6d1c7  42984  rhmqusspan  42985  grpods  42994  unitscyglem1  42995  unitscyglem2  42996  unitscyglem3  42997  unitscyglem4  42998  aks5lem7  43000  aks5  43004  prjspersym  43372  eldioph2b  43527  diophrex  43539  irrapxlem6  43587  pellex  43595  pellfundex  43646  lnrfg  43879  mpaaeu  43910  cvgdvgrat  45056  climsuse  46357  limsupre  46388  limcleqr  46391  limsuppnfdlem  46448  liminflelimsuplem  46522  limsupub2  46559  xlimclim2lem  46586  climxlim2  46593  cncficcgt0  46635  dvbdfbdioo  46677  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  stoweidlem28  46775  stoweidlem29  46776  stoweidlem52  46799  stoweidlem60  46807  fourierdlem39  46893  fourierdlem102  46955  fourierdlem103  46956  fourierdlem104  46957  fourierdlem114  46967  hspmbllem2  47374  nnsum4primesevenALTV  48599  imaf1co  49966