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 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

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

This theorem is referenced by:  xpdifid  6167  xpdifcnvepel  6168  fimaproj  8132  modmuladdnn0  13953  1arith  16988  prmgaplem5  17116  prmgapprmolem  17122  ffthiso  17989  chnso  18681  mhmid  19130  mhmmnd  19131  ghmgrp  19133  ghmqusnsg  19353  ghmquskerlem3  19357  ghmqusker  19358  ghmcmn  19902  ablfac2  20162  ringinvnz1ne0  20384  isdrng4  20826  drngidl  21366  rhmqusnsg  21406  rngqipring1  21437  isprmidlc  21453  qsidomlem2  21462  ssdifidlprm  21467  zringlpirlem1  21593  mp2pm2mplem4  22947  neiptopuni  23268  neiptoptop  23269  neiptopnei  23270  neitr  23318  hauscmplem  23544  2ndcomap  23596  lly1stc  23634  dissnref  23666  neitx  23745  cnextcn  24205  ustexsym  24354  ustex2sym  24355  ustex3sym  24356  trust  24367  utoptop  24372  restutop  24375  restutopopn  24376  ustuqtop1  24379  ustuqtop2  24380  ustuqtop3  24381  ustuqtop4  24382  utopreg  24390  ucncn  24422  fmucnd  24429  cfilufg  24430  trcfilu  24431  neipcfilu  24433  metustid  24692  metustsym  24693  metustexhalf  24694  metust  24696  cfilucfil  24697  metustbl  24704  psmetutop  24705  restmetu  24708  qdensere  24907  opnreen  24970  nmoleub2lem3  25255  ovolicc2lem4  25660  plydivlem4  26438  ulmuni  26536  dchrpt  27412  tgcgrtriv  28734  tgbtwntriv2  28737  tgbtwncom  28738  tgbtwnswapid  28742  tgbtwnintr  28743  tgbtwnouttr2  28745  tgtrisegint  28749  tgifscgr  28758  tgcgrxfr  28768  tgbtwnxfr  28780  motcgrg  28794  tgbtwnconn1lem3  28824  tgbtwnconn1  28825  tgbtwnconn3  28827  legval  28834  legov  28835  legov2  28836  legtrd  28839  legtri3  28840  legtrid  28841  ltgseg  28846  hlcgrex  28869  hlcgreulem  28870  colline  28904  tglnpt3  28908  miriso  28928  symquadlem  28947  krippenlem  28948  midexlem  28950  perpneq  28975  isperp2  28976  footexALT  28979  footex  28982  perpin  28986  perpdrag  28990  colperpexlem3  28994  colperpex  28995  opphllem  28997  mideulem  28998  midex  28999  oppne3  29005  oppnid  29008  opphllem3  29011  opphllem5  29013  opphllem6  29014  oppperpex  29015  opphl  29016  outpasch  29018  hpgne1  29024  hpgne2  29025  lnopp2hpgb  29026  colopp  29032  plngrotlem1  29050  plngrotlem3  29052  lnssplnglem  29054  plng3p  29060  lmieu  29074  symquadmid  29089  lnperpex  29094  trgcopy  29096  trgcopyeulem  29097  acopy  29125  acopyeu  29126  ragcgra  29127  perpeqlem  29131  inaghl  29143  leagne1  29147  leagne2  29148  leagne3  29149  leagne4  29150  cgrg3col4  29151  tgasa1  29156  prlnghpg  29177  perpprlng  29181  prlngex  29182  prlngmolem1  29183  prlngmolem2  29184  prlngmid2  29192  quadcgrprlng  29197  tgaltai  29198  f1otrg  29201  ttgbtwnid  29214  cnvbraval  32443  opsqrlem1  32473  rabfodom  32832  acunirnmpt  32985  acunirnmpt2  32986  acunirnmpt2f  32987  xrge0infss  33086  fsumiunle  33154  2exple2exp  33159  expevenpos  33160  wrdt2ind  33254  mgcf1o  33304  mndlactf1o  33331  gsummpt2d  33350  gsumwrd2dccatlem  33378  trsp2cyc  33424  cycpmrn  33444  tocyccntz  33445  cyc3evpm  33451  cyc3genpm  33453  cycpmgcl  33454  cycpmconjslem2  33456  cyc3conja  33458  archirngz  33490  archiabllem1a  33492  archiabllem1b  33493  archiabllem1  33494  archiabllem2a  33495  archiabllem2c  33496  archiabl  33499  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnlem4  33546  elrgspnsubrunlem1  33548  elrgspnsubrunlem2  33549  elrgspnsubrun  33550  erler  33566  elrlocbasi  33568  rlocaddval  33570  rlocmulval  33571  rlocf1  33575  rlocisunit  33577  fracfld  33610  imaslmod  33654  znfermltl  33662  nsgqusf1olem1  33703  lmhmqusker  33707  unitpidl1  33713  rhmquskerlem  33714  rhmimaidl  33721  mxidlprm  33734  mxidlirredi  33735  mxidlirred  33736  drngmxidlr  33741  opprqusplusg  33752  opprqusmulr  33754  qsdrngi  33758  qsdrnglem2  33759  dflringlem2  33766  dflring3  33768  dflring4  33769  rprmasso2  33797  rprmirredlem  33801  1arithidom  33808  pidufd  33814  1arithufdlem1  33815  1arithufdlem2  33816  1arithufdlem3  33817  1arithufdlem4  33818  dfufd2lem  33820  dfufd2  33821  esplymhp  33939  esplyfv1  33940  esplyfv  33941  esplyfval3  33943  esplyfval1  33944  lbslelsp  33969  dimval  33972  dimvalfi  33973  lssdimle  33979  lbsdiflsp0  33997  dimkerim  33998  fedgmul  34002  dimlssid  34003  extdg1id  34037  fldextrspunlsplem  34044  extdgfialglem1  34063  extdgfialg  34065  irngnminplynz  34083  fldext2chn  34099  constrext2chnlem  34121  constrfiss  34122  constrllcllem  34123  constrlccllem  34124  constrcccllem  34125  constrcn  34131  cos9thpiminplylem2  34154  txomap  34205  qtophaus  34207  pcmplfinf  34232  zarcls1  34240  zarclsun  34241  zarclsint  34243  zarclssn  34244  zarcmplem  34252  rhmpreimacn  34256  pstmxmet  34268  pnfneige0  34322  esumcst  34434  esum2d  34464  esumiun  34465  ddemeas  34607  signsply0  34919  signstres  34943  prodfzo03  34971  actfunsnf1o  34972  actfunsnrndisj  34973  tgoldbachgt  35031  poimirlem17  38269  poimirlem20  38272  itg2gt0cn  38307  fdc1  38378  lhprelat3N  40795  dihjat2  42186  aks4d1p8  42835  primrootspoweq0  42854  aks6d1c4  42872  aks6d1c6isolem1  42922  aks6d1c6isolem2  42923  aks6d1c6lem5  42925  aks6d1c7  42932  rhmqusspan  42933  grpods  42942  unitscyglem1  42943  unitscyglem2  42944  unitscyglem3  42945  unitscyglem4  42946  aks5lem7  42948  aks5  42952  prjspersym  43322  eldioph2b  43477  diophrex  43489  irrapxlem6  43537  pellex  43545  pellfundex  43596  lnrfg  43829  mpaaeu  43860  cvgdvgrat  45006  climsuse  46307  limsupre  46338  limcleqr  46341  limsuppnfdlem  46398  liminflelimsuplem  46472  limsupub2  46509  xlimclim2lem  46536  climxlim2  46543  cncficcgt0  46585  dvbdfbdioo  46627  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  stoweidlem28  46725  stoweidlem29  46726  stoweidlem52  46749  stoweidlem60  46757  fourierdlem39  46843  fourierdlem102  46905  fourierdlem103  46906  fourierdlem104  46907  fourierdlem114  46917  hspmbllem2  47324  nnsum4primesevenALTV  48549  imaf1co  49916