Theorem r19.29a 3144

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  xpdifid  6126  fimaproj  8077  modmuladdnn0  13838  1arith  16855  prmgaplem5  16983  prmgapprmolem  16989  ffthiso  17855  chnso  18547  mhmid  18993  mhmmnd  18994  ghmgrp  18996  ghmqusnsg  19211  ghmquskerlem3  19215  ghmqusker  19216  ghmcmn  19760  ablfac2  20020  ringinvnz1ne0  20235  rhmqusnsg  21240  rngqipring1  21271  zringlpirlem1  21417  mp2pm2mplem4  22753  neiptopuni  23074  neiptoptop  23075  neiptopnei  23076  neitr  23124  hauscmplem  23350  2ndcomap  23402  lly1stc  23440  dissnref  23472  neitx  23551  cnextcn  24011  ustexsym  24160  ustex2sym  24161  ustex3sym  24162  trust  24173  utoptop  24178  restutop  24181  restutopopn  24182  ustuqtop1  24185  ustuqtop2  24186  ustuqtop3  24187  ustuqtop4  24188  utopreg  24196  ucncn  24228  fmucnd  24235  cfilufg  24236  trcfilu  24237  neipcfilu  24239  metustid  24498  metustsym  24499  metustexhalf  24500  metust  24502  cfilucfil  24503  metustbl  24510  psmetutop  24511  restmetu  24514  qdensere  24713  opnreen  24776  nmoleub2lem3  25071  ovolicc2lem4  25477  plydivlem4  26260  ulmuni  26357  dchrpt  27234  tgcgrtriv  28556  tgbtwntriv2  28559  tgbtwncom  28560  tgbtwnswapid  28564  tgbtwnintr  28565  tgbtwnouttr2  28567  tgtrisegint  28571  tgifscgr  28580  tgcgrxfr  28590  tgbtwnxfr  28602  motcgrg  28616  tgbtwnconn1lem3  28646  tgbtwnconn1  28647  tgbtwnconn3  28649  legval  28656  legov  28657  legov2  28658  legtrd  28661  legtri3  28662  legtrid  28663  ltgseg  28668  hlcgrex  28688  hlcgreulem  28689  colline  28721  miriso  28742  symquadlem  28761  krippenlem  28762  midexlem  28764  perpneq  28786  isperp2  28787  footexALT  28790  footex  28793  perpdrag  28800  colperpexlem3  28804  colperpex  28805  opphllem  28807  mideulem  28808  midex  28809  oppne3  28815  oppnid  28818  opphllem3  28821  opphllem5  28823  opphllem6  28824  oppperpex  28825  opphl  28826  outpasch  28827  hpgne1  28833  hpgne2  28834  lnopp2hpgb  28835  colopp  28841  lmieu  28856  lnperpex  28875  trgcopy  28876  trgcopyeulem  28877  acopy  28905  acopyeu  28906  inaghl  28917  leagne1  28921  leagne2  28922  leagne3  28923  leagne4  28924  cgrg3col4  28925  tgasa1  28930  f1otrg  28943  ttgbtwnid  28956  cnvbraval  32185  opsqrlem1  32215  rabfodom  32580  acunirnmpt  32737  acunirnmpt2  32738  acunirnmpt2f  32739  xrge0infss  32840  fsumiunle  32910  2exple2exp  32926  expevenpos  32927  wrdt2ind  33035  mgcf1o  33085  mndlactf1o  33112  gsummpt2d  33132  gsumwrd2dccatlem  33159  trsp2cyc  33205  cycpmrn  33225  tocyccntz  33226  cyc3evpm  33232  cyc3genpm  33234  cycpmgcl  33235  cycpmconjslem2  33237  cyc3conja  33239  archirngz  33271  archiabllem1a  33273  archiabllem1b  33274  archiabllem1  33275  archiabllem2a  33276  archiabllem2c  33277  archiabl  33280  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  elrgspnsubrun  33331  erler  33347  elrlocbasi  33348  rlocaddval  33350  rlocmulval  33351  rlocf1  33355  isdrng4  33377  fracfld  33390  imaslmod  33434  znfermltl  33447  nsgqusf1olem1  33494  lmhmqusker  33498  unitpidl1  33505  rhmquskerlem  33506  rhmimaidl  33513  drngidl  33514  isprmidlc  33528  qsidomlem2  33534  ssdifidlprm  33539  mxidlprm  33551  mxidlirredi  33552  mxidlirred  33553  drngmxidlr  33559  opprqusplusg  33570  opprqusmulr  33572  qsdrngi  33576  qsdrnglem2  33577  rprmasso2  33607  rprmirredlem  33611  1arithidom  33618  pidufd  33624  1arithufdlem1  33625  1arithufdlem2  33626  1arithufdlem3  33627  1arithufdlem4  33628  dfufd2lem  33630  dfufd2  33631  esplymhp  33726  esplyfv1  33727  esplyfv  33728  esplyfval3  33730  lbslelsp  33754  dimval  33757  dimvalfi  33758  lssdimle  33764  lbsdiflsp0  33783  dimkerim  33784  fedgmul  33788  dimlssid  33789  extdg1id  33823  fldextrspunlsplem  33830  extdgfialglem1  33849  extdgfialg  33851  irngnminplynz  33869  fldext2chn  33885  constrext2chnlem  33907  constrfiss  33908  constrllcllem  33909  constrlccllem  33910  constrcccllem  33911  constrcn  33917  cos9thpiminplylem2  33940  txomap  33991  qtophaus  33993  pcmplfinf  34018  zarcls1  34026  zarclsun  34027  zarclsint  34029  zarclssn  34030  zarcmplem  34038  rhmpreimacn  34042  pstmxmet  34054  pnfneige0  34108  esumcst  34220  esum2d  34250  esumiun  34251  ddemeas  34393  signsply0  34708  signstres  34732  prodfzo03  34760  actfunsnf1o  34761  actfunsnrndisj  34762  tgoldbachgt  34820  poimirlem17  37838  poimirlem20  37841  itg2gt0cn  37876  fdc1  37947  lhprelat3N  40300  dihjat2  41691  aks4d1p8  42341  primrootspoweq0  42360  aks6d1c4  42378  aks6d1c6isolem1  42428  aks6d1c6isolem2  42429  aks6d1c6lem5  42431  aks6d1c7  42438  rhmqusspan  42439  grpods  42448  unitscyglem1  42449  unitscyglem2  42450  unitscyglem3  42451  unitscyglem4  42452  aks5lem7  42454  aks5  42458  prjspersym  42850  eldioph2b  43005  diophrex  43017  irrapxlem6  43069  pellex  43077  pellfundex  43128  lnrfg  43361  mpaaeu  43392  cvgdvgrat  44554  climsuse  45854  limsupre  45885  limcleqr  45888  limsuppnfdlem  45945  liminflelimsuplem  46019  limsupub2  46056  xlimclim2lem  46083  climxlim2  46090  cncficcgt0  46132  dvbdfbdioo  46174  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  stoweidlem28  46272  stoweidlem29  46273  stoweidlem52  46296  stoweidlem60  46304  fourierdlem39  46390  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem114  46464  hspmbllem2  46871  nnsum4primesevenALTV  48047  imaf1co  49400