Theorem r19.29a 3146

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  xpdifid  6126  fimaproj  8078  modmuladdnn0  13868  1arith  16889  prmgaplem5  17017  prmgapprmolem  17023  ffthiso  17889  chnso  18581  mhmid  19030  mhmmnd  19031  ghmgrp  19033  ghmqusnsg  19248  ghmquskerlem3  19252  ghmqusker  19253  ghmcmn  19797  ablfac2  20057  ringinvnz1ne0  20272  rhmqusnsg  21275  rngqipring1  21306  zringlpirlem1  21452  mp2pm2mplem4  22784  neiptopuni  23105  neiptoptop  23106  neiptopnei  23107  neitr  23155  hauscmplem  23381  2ndcomap  23433  lly1stc  23471  dissnref  23503  neitx  23582  cnextcn  24042  ustexsym  24191  ustex2sym  24192  ustex3sym  24193  trust  24204  utoptop  24209  restutop  24212  restutopopn  24213  ustuqtop1  24216  ustuqtop2  24217  ustuqtop3  24218  ustuqtop4  24219  utopreg  24227  ucncn  24259  fmucnd  24266  cfilufg  24267  trcfilu  24268  neipcfilu  24270  metustid  24529  metustsym  24530  metustexhalf  24531  metust  24533  cfilucfil  24534  metustbl  24541  psmetutop  24542  restmetu  24545  qdensere  24744  opnreen  24807  nmoleub2lem3  25092  ovolicc2lem4  25497  plydivlem4  26273  ulmuni  26370  dchrpt  27244  tgcgrtriv  28566  tgbtwntriv2  28569  tgbtwncom  28570  tgbtwnswapid  28574  tgbtwnintr  28575  tgbtwnouttr2  28577  tgtrisegint  28581  tgifscgr  28590  tgcgrxfr  28600  tgbtwnxfr  28612  motcgrg  28626  tgbtwnconn1lem3  28656  tgbtwnconn1  28657  tgbtwnconn3  28659  legval  28666  legov  28667  legov2  28668  legtrd  28671  legtri3  28672  legtrid  28673  ltgseg  28678  hlcgrex  28698  hlcgreulem  28699  colline  28731  miriso  28752  symquadlem  28771  krippenlem  28772  midexlem  28774  perpneq  28796  isperp2  28797  footexALT  28800  footex  28803  perpdrag  28810  colperpexlem3  28814  colperpex  28815  opphllem  28817  mideulem  28818  midex  28819  oppne3  28825  oppnid  28828  opphllem3  28831  opphllem5  28833  opphllem6  28834  oppperpex  28835  opphl  28836  outpasch  28837  hpgne1  28843  hpgne2  28844  lnopp2hpgb  28845  colopp  28851  lmieu  28866  lnperpex  28885  trgcopy  28886  trgcopyeulem  28887  acopy  28915  acopyeu  28916  inaghl  28927  leagne1  28931  leagne2  28932  leagne3  28933  leagne4  28934  cgrg3col4  28935  tgasa1  28940  f1otrg  28953  ttgbtwnid  28966  cnvbraval  32196  opsqrlem1  32226  rabfodom  32590  acunirnmpt  32747  acunirnmpt2  32748  acunirnmpt2f  32749  xrge0infss  32848  fsumiunle  32917  2exple2exp  32933  expevenpos  32934  wrdt2ind  33028  mgcf1o  33078  mndlactf1o  33105  gsummpt2d  33125  gsumwrd2dccatlem  33153  trsp2cyc  33199  cycpmrn  33219  tocyccntz  33220  cyc3evpm  33226  cyc3genpm  33228  cycpmgcl  33229  cycpmconjslem2  33231  cyc3conja  33233  archirngz  33265  archiabllem1a  33267  archiabllem1b  33268  archiabllem1  33269  archiabllem2a  33270  archiabllem2c  33271  archiabl  33274  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem4  33321  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  elrgspnsubrun  33325  erler  33341  elrlocbasi  33342  rlocaddval  33344  rlocmulval  33345  rlocf1  33349  isdrng4  33371  fracfld  33384  imaslmod  33428  znfermltl  33441  nsgqusf1olem1  33488  lmhmqusker  33492  unitpidl1  33499  rhmquskerlem  33500  rhmimaidl  33507  drngidl  33508  isprmidlc  33522  qsidomlem2  33528  ssdifidlprm  33533  mxidlprm  33545  mxidlirredi  33546  mxidlirred  33547  drngmxidlr  33553  opprqusplusg  33564  opprqusmulr  33566  qsdrngi  33570  qsdrnglem2  33571  rprmasso2  33601  rprmirredlem  33605  1arithidom  33612  pidufd  33618  1arithufdlem1  33619  1arithufdlem2  33620  1arithufdlem3  33621  1arithufdlem4  33622  dfufd2lem  33624  dfufd2  33625  esplymhp  33727  esplyfv1  33728  esplyfv  33729  esplyfval3  33731  esplyfval1  33732  lbslelsp  33757  dimval  33760  dimvalfi  33761  lssdimle  33767  lbsdiflsp0  33786  dimkerim  33787  fedgmul  33791  dimlssid  33792  extdg1id  33826  fldextrspunlsplem  33833  extdgfialglem1  33852  extdgfialg  33854  irngnminplynz  33872  fldext2chn  33888  constrext2chnlem  33910  constrfiss  33911  constrllcllem  33912  constrlccllem  33913  constrcccllem  33914  constrcn  33920  cos9thpiminplylem2  33943  txomap  33994  qtophaus  33996  pcmplfinf  34021  zarcls1  34029  zarclsun  34030  zarclsint  34032  zarclssn  34033  zarcmplem  34041  rhmpreimacn  34045  pstmxmet  34057  pnfneige0  34111  esumcst  34223  esum2d  34253  esumiun  34254  ddemeas  34396  signsply0  34711  signstres  34735  prodfzo03  34763  actfunsnf1o  34764  actfunsnrndisj  34765  tgoldbachgt  34823  poimirlem17  37972  poimirlem20  37975  itg2gt0cn  38010  fdc1  38081  lhprelat3N  40500  dihjat2  41891  aks4d1p8  42540  primrootspoweq0  42559  aks6d1c4  42577  aks6d1c6isolem1  42627  aks6d1c6isolem2  42628  aks6d1c6lem5  42630  aks6d1c7  42637  rhmqusspan  42638  grpods  42647  unitscyglem1  42648  unitscyglem2  42649  unitscyglem3  42650  unitscyglem4  42651  aks5lem7  42653  aks5  42657  prjspersym  43054  eldioph2b  43209  diophrex  43221  irrapxlem6  43273  pellex  43281  pellfundex  43332  lnrfg  43565  mpaaeu  43596  cvgdvgrat  44758  climsuse  46056  limsupre  46087  limcleqr  46090  limsuppnfdlem  46147  liminflelimsuplem  46221  limsupub2  46258  xlimclim2lem  46285  climxlim2  46292  cncficcgt0  46334  dvbdfbdioo  46376  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  stoweidlem28  46474  stoweidlem29  46475  stoweidlem52  46498  stoweidlem60  46506  fourierdlem39  46592  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem114  46666  hspmbllem2  47073  nnsum4primesevenALTV  48289  imaf1co  49642