Theorem r19.29a 3173

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  xpdifid  6156  xpdifcnvepel  6157  fimaproj  8119  modmuladdnn0  13939  1arith  16975  prmgaplem5  17103  prmgapprmolem  17109  ffthiso  17976  chnso  18668  mhmid  19117  mhmmnd  19118  ghmgrp  19120  ghmqusnsg  19340  ghmquskerlem3  19344  ghmqusker  19345  ghmcmn  19889  ablfac2  20149  ringinvnz1ne0  20371  rhmqusnsg  21384  rngqipring1  21415  isprmidlc  21431  qsidomlem2  21438  ssdifidlprm  21443  zringlpirlem1  21569  mp2pm2mplem4  22923  neiptopuni  23244  neiptoptop  23245  neiptopnei  23246  neitr  23294  hauscmplem  23520  2ndcomap  23572  lly1stc  23610  dissnref  23642  neitx  23721  cnextcn  24181  ustexsym  24330  ustex2sym  24331  ustex3sym  24332  trust  24343  utoptop  24348  restutop  24351  restutopopn  24352  ustuqtop1  24355  ustuqtop2  24356  ustuqtop3  24357  ustuqtop4  24358  utopreg  24366  ucncn  24398  fmucnd  24405  cfilufg  24406  trcfilu  24407  neipcfilu  24409  metustid  24668  metustsym  24669  metustexhalf  24670  metust  24672  cfilucfil  24673  metustbl  24680  psmetutop  24681  restmetu  24684  qdensere  24883  opnreen  24946  nmoleub2lem3  25231  ovolicc2lem4  25636  plydivlem4  26414  ulmuni  26509  dchrpt  27385  tgcgrtriv  28707  tgbtwntriv2  28710  tgbtwncom  28711  tgbtwnswapid  28715  tgbtwnintr  28716  tgbtwnouttr2  28718  tgtrisegint  28722  tgifscgr  28731  tgcgrxfr  28741  tgbtwnxfr  28753  motcgrg  28767  tgbtwnconn1lem3  28797  tgbtwnconn1  28798  tgbtwnconn3  28800  legval  28807  legov  28808  legov2  28809  legtrd  28812  legtri3  28813  legtrid  28814  ltgseg  28819  hlcgrex  28839  hlcgreulem  28840  colline  28873  tglnpt3  28877  miriso  28897  symquadlem  28916  krippenlem  28917  midexlem  28919  perpneq  28941  isperp2  28942  footexALT  28945  footex  28948  perpdrag  28955  colperpexlem3  28959  colperpex  28960  opphllem  28962  mideulem  28963  midex  28964  oppne3  28970  oppnid  28973  opphllem3  28976  opphllem5  28978  opphllem6  28979  oppperpex  28980  opphl  28981  outpasch  28982  hpgne1  28988  hpgne2  28989  lnopp2hpgb  28990  colopp  28996  plngrotlem1  29013  plngrotlem3  29015  lnssplnglem  29017  plng3p  29019  lmieu  29032  lnperpex  29051  trgcopy  29052  trgcopyeulem  29053  acopy  29081  acopyeu  29082  inaghl  29093  leagne1  29097  leagne2  29098  leagne3  29099  leagne4  29100  cgrg3col4  29101  tgasa1  29106  f1otrg  29125  ttgbtwnid  29138  cnvbraval  32367  opsqrlem1  32397  rabfodom  32757  acunirnmpt  32912  acunirnmpt2  32913  acunirnmpt2f  32914  xrge0infss  33013  fsumiunle  33081  2exple2exp  33086  expevenpos  33087  wrdt2ind  33181  mgcf1o  33231  mndlactf1o  33258  gsummpt2d  33277  gsumwrd2dccatlem  33305  trsp2cyc  33351  cycpmrn  33371  tocyccntz  33372  cyc3evpm  33378  cyc3genpm  33380  cycpmgcl  33381  cycpmconjslem2  33383  cyc3conja  33385  archirngz  33417  archiabllem1a  33419  archiabllem1b  33420  archiabllem1  33421  archiabllem2a  33422  archiabllem2c  33423  archiabl  33426  elrgspnlem1  33470  elrgspnlem2  33471  elrgspnlem4  33473  elrgspnsubrunlem1  33475  elrgspnsubrunlem2  33476  elrgspnsubrun  33477  erler  33493  elrlocbasi  33495  rlocaddval  33497  rlocmulval  33498  rlocf1  33502  rlocisunit  33504  isdrng4  33526  fracfld  33539  imaslmod  33583  znfermltl  33591  nsgqusf1olem1  33633  lmhmqusker  33637  unitpidl1  33643  rhmquskerlem  33644  rhmimaidl  33651  drngidl  33652  mxidlprm  33665  mxidlirredi  33666  mxidlirred  33667  drngmxidlr  33672  opprqusplusg  33683  opprqusmulr  33685  qsdrngi  33689  qsdrnglem2  33690  dflringlem2  33697  dflring3  33699  dflring4  33700  rprmasso2  33728  rprmirredlem  33732  1arithidom  33739  pidufd  33745  1arithufdlem1  33746  1arithufdlem2  33747  1arithufdlem3  33748  1arithufdlem4  33749  dfufd2lem  33751  dfufd2  33752  esplymhp  33870  esplyfv1  33871  esplyfv  33872  esplyfval3  33874  esplyfval1  33875  lbslelsp  33900  dimval  33903  dimvalfi  33904  lssdimle  33910  lbsdiflsp0  33928  dimkerim  33929  fedgmul  33933  dimlssid  33934  extdg1id  33968  fldextrspunlsplem  33975  extdgfialglem1  33994  extdgfialg  33996  irngnminplynz  34014  fldext2chn  34030  constrext2chnlem  34052  constrfiss  34053  constrllcllem  34054  constrlccllem  34055  constrcccllem  34056  constrcn  34062  cos9thpiminplylem2  34085  txomap  34136  qtophaus  34138  pcmplfinf  34163  zarcls1  34171  zarclsun  34172  zarclsint  34174  zarclssn  34175  zarcmplem  34183  rhmpreimacn  34187  pstmxmet  34199  pnfneige0  34253  esumcst  34365  esum2d  34395  esumiun  34396  ddemeas  34538  signsply0  34850  signstres  34874  prodfzo03  34902  actfunsnf1o  34903  actfunsnrndisj  34904  tgoldbachgt  34962  poimirlem17  38143  poimirlem20  38146  itg2gt0cn  38181  fdc1  38252  lhprelat3N  40671  dihjat2  42062  aks4d1p8  42711  primrootspoweq0  42730  aks6d1c4  42748  aks6d1c6isolem1  42798  aks6d1c6isolem2  42799  aks6d1c6lem5  42801  aks6d1c7  42808  rhmqusspan  42809  grpods  42818  unitscyglem1  42819  unitscyglem2  42820  unitscyglem3  42821  unitscyglem4  42822  aks5lem7  42824  aks5  42828  prjspersym  43196  eldioph2b  43351  diophrex  43363  irrapxlem6  43411  pellex  43419  pellfundex  43470  lnrfg  43703  mpaaeu  43734  cvgdvgrat  44882  climsuse  46183  limsupre  46214  limcleqr  46217  limsuppnfdlem  46274  liminflelimsuplem  46348  limsupub2  46385  xlimclim2lem  46412  climxlim2  46419  cncficcgt0  46461  dvbdfbdioo  46503  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  stoweidlem28  46601  stoweidlem29  46602  stoweidlem52  46625  stoweidlem60  46633  fourierdlem39  46719  fourierdlem102  46781  fourierdlem103  46782  fourierdlem104  46783  fourierdlem114  46793  hspmbllem2  47200  nnsum4primesevenALTV  48422  imaf1co  49785