Theorem r19.29a 3169

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  xpdifid  6148  fimaproj  8108  modmuladdnn0  13921  1arith  16953  prmgaplem5  17081  prmgapprmolem  17087  ffthiso  17954  chnso  18646  mhmid  19095  mhmmnd  19096  ghmgrp  19098  ghmqusnsg  19312  ghmquskerlem3  19316  ghmqusker  19317  ghmcmn  19861  ablfac2  20121  ringinvnz1ne0  20336  rhmqusnsg  21342  rngqipring1  21373  zringlpirlem1  21501  mp2pm2mplem4  22856  neiptopuni  23177  neiptoptop  23178  neiptopnei  23179  neitr  23227  hauscmplem  23453  2ndcomap  23505  lly1stc  23543  dissnref  23575  neitx  23654  cnextcn  24114  ustexsym  24263  ustex2sym  24264  ustex3sym  24265  trust  24276  utoptop  24281  restutop  24284  restutopopn  24285  ustuqtop1  24288  ustuqtop2  24289  ustuqtop3  24290  ustuqtop4  24291  utopreg  24299  ucncn  24331  fmucnd  24338  cfilufg  24339  trcfilu  24340  neipcfilu  24342  metustid  24601  metustsym  24602  metustexhalf  24603  metust  24605  cfilucfil  24606  metustbl  24613  psmetutop  24614  restmetu  24617  qdensere  24816  opnreen  24879  nmoleub2lem3  25164  ovolicc2lem4  25569  plydivlem4  26347  ulmuni  26442  dchrpt  27318  tgcgrtriv  28640  tgbtwntriv2  28643  tgbtwncom  28644  tgbtwnswapid  28648  tgbtwnintr  28649  tgbtwnouttr2  28651  tgtrisegint  28655  tgifscgr  28664  tgcgrxfr  28674  tgbtwnxfr  28686  motcgrg  28700  tgbtwnconn1lem3  28730  tgbtwnconn1  28731  tgbtwnconn3  28733  legval  28740  legov  28741  legov2  28742  legtrd  28745  legtri3  28746  legtrid  28747  ltgseg  28752  hlcgrex  28772  hlcgreulem  28773  colline  28805  miriso  28826  symquadlem  28845  krippenlem  28846  midexlem  28848  perpneq  28870  isperp2  28871  footexALT  28874  footex  28877  perpdrag  28884  colperpexlem3  28888  colperpex  28889  opphllem  28891  mideulem  28892  midex  28893  oppne3  28899  oppnid  28902  opphllem3  28905  opphllem5  28907  opphllem6  28908  oppperpex  28909  opphl  28910  outpasch  28911  hpgne1  28917  hpgne2  28918  lnopp2hpgb  28919  colopp  28925  lmieu  28940  lnperpex  28959  trgcopy  28960  trgcopyeulem  28961  acopy  28989  acopyeu  28990  inaghl  29001  leagne1  29005  leagne2  29006  leagne3  29007  leagne4  29008  cgrg3col4  29009  tgasa1  29014  f1otrg  29027  ttgbtwnid  29040  cnvbraval  32269  opsqrlem1  32299  rabfodom  32663  acunirnmpt  32821  acunirnmpt2  32822  acunirnmpt2f  32823  xrge0infss  32922  fsumiunle  32991  2exple2exp  32996  expevenpos  32997  wrdt2ind  33091  mgcf1o  33141  mndlactf1o  33168  gsummpt2d  33189  gsumwrd2dccatlem  33217  trsp2cyc  33263  cycpmrn  33283  tocyccntz  33284  cyc3evpm  33290  cyc3genpm  33292  cycpmgcl  33293  cycpmconjslem2  33295  cyc3conja  33297  archirngz  33329  archiabllem1a  33331  archiabllem1b  33332  archiabllem1  33333  archiabllem2a  33334  archiabllem2c  33335  archiabl  33338  elrgspnlem1  33383  elrgspnlem2  33384  elrgspnlem4  33386  elrgspnsubrunlem1  33388  elrgspnsubrunlem2  33389  elrgspnsubrun  33390  erler  33406  elrlocbasi  33408  rlocaddval  33410  rlocmulval  33411  rlocf1  33415  rlocisunit  33417  isdrng4  33442  fracfld  33455  imaslmod  33499  znfermltl  33512  nsgqusf1olem1  33559  lmhmqusker  33563  unitpidl1  33570  rhmquskerlem  33571  rhmimaidl  33578  drngidl  33579  isprmidlc  33593  qsidomlem2  33600  ssdifidlprm  33605  mxidlprm  33618  mxidlirredi  33619  mxidlirred  33620  drngmxidlr  33626  opprqusplusg  33637  opprqusmulr  33639  qsdrngi  33643  qsdrnglem2  33644  dflringlem2  33651  dflring3  33653  dflring4  33654  rprmasso2  33682  rprmirredlem  33686  1arithidom  33693  pidufd  33699  1arithufdlem1  33700  1arithufdlem2  33701  1arithufdlem3  33702  1arithufdlem4  33703  dfufd2lem  33705  dfufd2  33706  esplymhp  33825  esplyfv1  33826  esplyfv  33827  esplyfval3  33829  esplyfval1  33830  lbslelsp  33855  dimval  33858  dimvalfi  33859  lssdimle  33865  lbsdiflsp0  33883  dimkerim  33884  fedgmul  33888  dimlssid  33889  extdg1id  33923  fldextrspunlsplem  33930  extdgfialglem1  33949  extdgfialg  33951  irngnminplynz  33969  fldext2chn  33985  constrext2chnlem  34007  constrfiss  34008  constrllcllem  34009  constrlccllem  34010  constrcccllem  34011  constrcn  34017  cos9thpiminplylem2  34040  txomap  34091  qtophaus  34093  pcmplfinf  34118  zarcls1  34126  zarclsun  34127  zarclsint  34129  zarclssn  34130  zarcmplem  34138  rhmpreimacn  34142  pstmxmet  34154  pnfneige0  34208  esumcst  34320  esum2d  34350  esumiun  34351  ddemeas  34493  signsply0  34805  signstres  34829  prodfzo03  34857  actfunsnf1o  34858  actfunsnrndisj  34859  tgoldbachgt  34917  poimirlem17  38096  poimirlem20  38099  itg2gt0cn  38134  fdc1  38205  lhprelat3N  40624  dihjat2  42015  aks4d1p8  42664  primrootspoweq0  42683  aks6d1c4  42701  aks6d1c6isolem1  42751  aks6d1c6isolem2  42752  aks6d1c6lem5  42754  aks6d1c7  42761  rhmqusspan  42762  grpods  42771  unitscyglem1  42772  unitscyglem2  42773  unitscyglem3  42774  unitscyglem4  42775  aks5lem7  42777  aks5  42781  prjspersym  43149  eldioph2b  43304  diophrex  43316  irrapxlem6  43364  pellex  43372  pellfundex  43423  lnrfg  43656  mpaaeu  43687  cvgdvgrat  44849  climsuse  46144  limsupre  46175  limcleqr  46178  limsuppnfdlem  46235  liminflelimsuplem  46309  limsupub2  46346  xlimclim2lem  46373  climxlim2  46380  cncficcgt0  46422  dvbdfbdioo  46464  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  stoweidlem28  46562  stoweidlem29  46563  stoweidlem52  46586  stoweidlem60  46594  fourierdlem39  46680  fourierdlem102  46742  fourierdlem103  46743  fourierdlem104  46744  fourierdlem114  46754  hspmbllem2  47161  nnsum4primesevenALTV  48383  imaf1co  49736