Theorem r19.29a 3149

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 3144	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3060

This theorem is referenced by:  xpdifid  6170  fimaproj  8143  modmuladdnn0  13939  1arith  16948  prmgaplem5  17076  prmgapprmolem  17082  ffthiso  17952  mhmid  19055  mhmmnd  19056  ghmgrp  19058  ghmqusnsg  19274  ghmquskerlem3  19278  ghmqusker  19279  ghmcmn  19822  ablfac2  20082  ringinvnz1ne0  20270  rhmqusnsg  21262  rngqipring1  21293  zringlpirlem1  21440  mp2pm2mplem4  22782  neiptopuni  23103  neiptoptop  23104  neiptopnei  23105  neitr  23153  hauscmplem  23379  2ndcomap  23431  lly1stc  23469  dissnref  23501  neitx  23580  cnextcn  24040  ustexsym  24189  ustex2sym  24190  ustex3sym  24191  trust  24203  utoptop  24208  restutop  24211  restutopopn  24212  ustuqtop1  24215  ustuqtop2  24216  ustuqtop3  24217  ustuqtop4  24218  utopreg  24226  ucncn  24258  fmucnd  24265  cfilufg  24266  trcfilu  24267  neipcfilu  24269  metustid  24530  metustsym  24531  metustexhalf  24532  metust  24534  cfilucfil  24535  metustbl  24542  psmetutop  24543  restmetu  24546  qdensere  24745  opnreen  24808  nmoleub2lem3  25103  ovolicc2lem4  25510  plydivlem4  26293  ulmuni  26390  dchrpt  27266  tgcgrtriv  28447  tgbtwntriv2  28450  tgbtwncom  28451  tgbtwnswapid  28455  tgbtwnintr  28456  tgbtwnouttr2  28458  tgtrisegint  28462  tgifscgr  28471  tgcgrxfr  28481  tgbtwnxfr  28493  motcgrg  28507  tgbtwnconn1lem3  28537  tgbtwnconn1  28538  tgbtwnconn3  28540  legval  28547  legov  28548  legov2  28549  legtrd  28552  legtri3  28553  legtrid  28554  ltgseg  28559  hlcgrex  28579  hlcgreulem  28580  colline  28612  miriso  28633  symquadlem  28652  krippenlem  28653  midexlem  28655  perpneq  28677  isperp2  28678  footexALT  28681  footex  28684  perpdrag  28691  colperpexlem3  28695  colperpex  28696  opphllem  28698  mideulem  28699  midex  28700  oppne3  28706  oppnid  28709  opphllem3  28712  opphllem5  28714  opphllem6  28715  oppperpex  28716  opphl  28717  outpasch  28718  hpgne1  28724  hpgne2  28725  lnopp2hpgb  28726  colopp  28732  lmieu  28747  lnperpex  28766  trgcopy  28767  trgcopyeulem  28768  acopy  28796  acopyeu  28797  inaghl  28808  leagne1  28812  leagne2  28813  leagne3  28814  leagne4  28815  cgrg3col4  28816  tgasa1  28821  f1otrg  28834  ttgbtwnid  28848  cnvbraval  32076  opsqrlem1  32106  rabfodom  32471  acunirnmpt  32616  acunirnmpt2  32617  acunirnmpt2f  32618  xrge0infss  32711  fsumiunle  32778  2exple2exp  32781  wrdt2ind  32885  mgcf1o  32939  chnso  32950  mndlactf1o  32981  gsummpt2d  32998  gsumwrd2dccatlem  33015  trsp2cyc  33089  cycpmrn  33109  tocyccntz  33110  cyc3evpm  33116  cyc3genpm  33118  cycpmgcl  33119  cycpmconjslem2  33121  cyc3conja  33123  archirngz  33142  archiabllem1a  33144  archiabllem1b  33145  archiabllem1  33146  archiabllem2a  33147  archiabllem2c  33148  archiabl  33151  elrgspnlem1  33192  elrgspnlem2  33193  elrgspnlem4  33195  elrgspnsubrunlem1  33197  elrgspnsubrunlem2  33198  elrgspnsubrun  33199  erler  33215  elrlocbasi  33216  rlocaddval  33218  rlocmulval  33219  rlocf1  33223  isdrng4  33244  fracfld  33256  imaslmod  33322  znfermltl  33335  nsgqusf1olem1  33382  lmhmqusker  33386  unitpidl1  33393  rhmquskerlem  33394  rhmimaidl  33401  drngidl  33402  isprmidlc  33416  qsidomlem2  33422  ssdifidlprm  33427  mxidlprm  33439  mxidlirredi  33440  mxidlirred  33441  drngmxidlr  33447  opprqusplusg  33458  opprqusmulr  33460  qsdrngi  33464  qsdrnglem2  33465  rprmasso2  33495  rprmirredlem  33499  1arithidom  33506  pidufd  33512  1arithufdlem1  33513  1arithufdlem2  33514  1arithufdlem3  33515  1arithufdlem4  33516  dfufd2lem  33518  dfufd2  33519  lbslelsp  33589  dimval  33592  dimvalfi  33593  lssdimle  33599  lbsdiflsp0  33618  dimkerim  33619  fedgmul  33623  dimlssid  33624  extdg1id  33657  fldextrspunlsplem  33664  irngnminplynz  33696  fldext2chn  33710  txomap  33774  qtophaus  33776  pcmplfinf  33801  zarcls1  33809  zarclsun  33810  zarclsint  33812  zarclssn  33813  zarcmplem  33821  rhmpreimacn  33825  pstmxmet  33837  pnfneige0  33891  esumcst  34005  esum2d  34035  esumiun  34036  ddemeas  34178  signsply0  34507  signstres  34531  prodfzo03  34559  actfunsnf1o  34560  actfunsnrndisj  34561  tgoldbachgt  34619  poimirlem17  37585  poimirlem20  37588  itg2gt0cn  37623  fdc1  37694  lhprelat3N  39983  dihjat2  41374  aks4d1p8  42029  primrootspoweq0  42048  aks6d1c4  42066  aks6d1c6isolem1  42116  aks6d1c6isolem2  42117  aks6d1c6lem5  42119  aks6d1c7  42126  rhmqusspan  42127  grpods  42136  unitscyglem1  42137  unitscyglem2  42138  unitscyglem3  42139  unitscyglem4  42140  aks5lem7  42142  aks5  42146  prjspersym  42562  eldioph2b  42719  diophrex  42731  irrapxlem6  42783  pellex  42791  pellfundex  42842  lnrfg  43076  mpaaeu  43107  cvgdvgrat  44277  climsuse  45568  limsupre  45601  limcleqr  45604  limsuppnfdlem  45661  limsupub2  45772  xlimclim2lem  45799  climxlim2  45806  cncficcgt0  45848  dvbdfbdioo  45890  ioodvbdlimc1lem2  45892  ioodvbdlimc2lem  45894  stoweidlem28  45988  stoweidlem29  45989  stoweidlem52  46012  stoweidlem60  46020  fourierdlem39  46106  fourierdlem102  46168  fourierdlem103  46169  fourierdlem104  46170  fourierdlem114  46180  hspmbllem2  46587  nnsum4primesevenALTV  47734