Theorem r19.29a 3179

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  xpdifid  6166  xpdifcnvepel  6167  fimaproj  8131  modmuladdnn0  13951  1arith  16987  prmgaplem5  17115  prmgapprmolem  17121  ffthiso  17988  chnso  18680  mhmid  19129  mhmmnd  19130  ghmgrp  19132  ghmqusnsg  19352  ghmquskerlem3  19356  ghmqusker  19357  ghmcmn  19901  ablfac2  20161  ringinvnz1ne0  20383  rhmqusnsg  21396  rngqipring1  21427  isprmidlc  21443  qsidomlem2  21450  ssdifidlprm  21455  zringlpirlem1  21581  mp2pm2mplem4  22935  neiptopuni  23256  neiptoptop  23257  neiptopnei  23258  neitr  23306  hauscmplem  23532  2ndcomap  23584  lly1stc  23622  dissnref  23654  neitx  23733  cnextcn  24193  ustexsym  24342  ustex2sym  24343  ustex3sym  24344  trust  24355  utoptop  24360  restutop  24363  restutopopn  24364  ustuqtop1  24367  ustuqtop2  24368  ustuqtop3  24369  ustuqtop4  24370  utopreg  24378  ucncn  24410  fmucnd  24417  cfilufg  24418  trcfilu  24419  neipcfilu  24421  metustid  24680  metustsym  24681  metustexhalf  24682  metust  24684  cfilucfil  24685  metustbl  24692  psmetutop  24693  restmetu  24696  qdensere  24895  opnreen  24958  nmoleub2lem3  25243  ovolicc2lem4  25648  plydivlem4  26426  ulmuni  26521  dchrpt  27397  tgcgrtriv  28719  tgbtwntriv2  28722  tgbtwncom  28723  tgbtwnswapid  28727  tgbtwnintr  28728  tgbtwnouttr2  28730  tgtrisegint  28734  tgifscgr  28743  tgcgrxfr  28753  tgbtwnxfr  28765  motcgrg  28779  tgbtwnconn1lem3  28809  tgbtwnconn1  28810  tgbtwnconn3  28812  legval  28819  legov  28820  legov2  28821  legtrd  28824  legtri3  28825  legtrid  28826  ltgseg  28831  hlcgrex  28851  hlcgreulem  28852  colline  28885  tglnpt3  28889  miriso  28909  symquadlem  28928  krippenlem  28929  midexlem  28931  perpneq  28953  isperp2  28954  footexALT  28957  footex  28960  perpin  28964  perpdrag  28968  colperpexlem3  28972  colperpex  28973  opphllem  28975  mideulem  28976  midex  28977  oppne3  28983  oppnid  28986  opphllem3  28989  opphllem5  28991  opphllem6  28992  oppperpex  28993  opphl  28994  outpasch  28996  hpgne1  29002  hpgne2  29003  lnopp2hpgb  29004  colopp  29010  plngrotlem1  29027  plngrotlem3  29029  lnssplnglem  29031  plng3p  29037  lmieu  29051  lnperpex  29070  trgcopy  29072  trgcopyeulem  29073  acopy  29101  acopyeu  29102  ragcgra  29103  perpeqlem  29105  inaghl  29117  leagne1  29121  leagne2  29122  leagne3  29123  leagne4  29124  cgrg3col4  29125  tgasa1  29130  prlnghpg  29151  perpprlng  29153  prlngex  29154  prlngmolem1  29155  prlngmolem2  29156  f1otrg  29161  ttgbtwnid  29174  cnvbraval  32403  opsqrlem1  32433  rabfodom  32792  acunirnmpt  32945  acunirnmpt2  32946  acunirnmpt2f  32947  xrge0infss  33046  fsumiunle  33114  2exple2exp  33119  expevenpos  33120  wrdt2ind  33214  mgcf1o  33264  mndlactf1o  33291  gsummpt2d  33310  gsumwrd2dccatlem  33338  trsp2cyc  33384  cycpmrn  33404  tocyccntz  33405  cyc3evpm  33411  cyc3genpm  33413  cycpmgcl  33414  cycpmconjslem2  33416  cyc3conja  33418  archirngz  33450  archiabllem1a  33452  archiabllem1b  33453  archiabllem1  33454  archiabllem2a  33455  archiabllem2c  33456  archiabl  33459  elrgspnlem1  33503  elrgspnlem2  33504  elrgspnlem4  33506  elrgspnsubrunlem1  33508  elrgspnsubrunlem2  33509  elrgspnsubrun  33510  erler  33526  elrlocbasi  33528  rlocaddval  33530  rlocmulval  33531  rlocf1  33535  rlocisunit  33537  isdrng4  33559  fracfld  33572  imaslmod  33616  znfermltl  33624  nsgqusf1olem1  33666  lmhmqusker  33670  unitpidl1  33676  rhmquskerlem  33677  rhmimaidl  33684  drngidl  33685  mxidlprm  33698  mxidlirredi  33699  mxidlirred  33700  drngmxidlr  33705  opprqusplusg  33716  opprqusmulr  33718  qsdrngi  33722  qsdrnglem2  33723  dflringlem2  33730  dflring3  33732  dflring4  33733  rprmasso2  33761  rprmirredlem  33765  1arithidom  33772  pidufd  33778  1arithufdlem1  33779  1arithufdlem2  33780  1arithufdlem3  33781  1arithufdlem4  33782  dfufd2lem  33784  dfufd2  33785  esplymhp  33903  esplyfv1  33904  esplyfv  33905  esplyfval3  33907  esplyfval1  33908  lbslelsp  33933  dimval  33936  dimvalfi  33937  lssdimle  33943  lbsdiflsp0  33961  dimkerim  33962  fedgmul  33966  dimlssid  33967  extdg1id  34001  fldextrspunlsplem  34008  extdgfialglem1  34027  extdgfialg  34029  irngnminplynz  34047  fldext2chn  34063  constrext2chnlem  34085  constrfiss  34086  constrllcllem  34087  constrlccllem  34088  constrcccllem  34089  constrcn  34095  cos9thpiminplylem2  34118  txomap  34169  qtophaus  34171  pcmplfinf  34196  zarcls1  34204  zarclsun  34205  zarclsint  34207  zarclssn  34208  zarcmplem  34216  rhmpreimacn  34220  pstmxmet  34232  pnfneige0  34286  esumcst  34398  esum2d  34428  esumiun  34429  ddemeas  34571  signsply0  34883  signstres  34907  prodfzo03  34935  actfunsnf1o  34936  actfunsnrndisj  34937  tgoldbachgt  34995  poimirlem17  38211  poimirlem20  38214  itg2gt0cn  38249  fdc1  38320  lhprelat3N  40739  dihjat2  42130  aks4d1p8  42779  primrootspoweq0  42798  aks6d1c4  42816  aks6d1c6isolem1  42866  aks6d1c6isolem2  42867  aks6d1c6lem5  42869  aks6d1c7  42876  rhmqusspan  42877  grpods  42886  unitscyglem1  42887  unitscyglem2  42888  unitscyglem3  42889  unitscyglem4  42890  aks5lem7  42892  aks5  42896  prjspersym  43266  eldioph2b  43421  diophrex  43433  irrapxlem6  43481  pellex  43489  pellfundex  43540  lnrfg  43773  mpaaeu  43804  cvgdvgrat  44950  climsuse  46251  limsupre  46282  limcleqr  46285  limsuppnfdlem  46342  liminflelimsuplem  46416  limsupub2  46453  xlimclim2lem  46480  climxlim2  46487  cncficcgt0  46529  dvbdfbdioo  46571  ioodvbdlimc1lem2  46573  ioodvbdlimc2lem  46575  stoweidlem28  46669  stoweidlem29  46670  stoweidlem52  46693  stoweidlem60  46701  fourierdlem39  46787  fourierdlem102  46849  fourierdlem103  46850  fourierdlem104  46851  fourierdlem114  46861  hspmbllem2  47268  nnsum4primesevenALTV  48490  imaf1co  49853