Theorem r19.29a 3154

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-rex 3063

This theorem is referenced by:  xpdifid  6157  fimaproj  8115  modmuladdnn0  13876  1arith  16856  prmgaplem5  16984  prmgapprmolem  16990  ffthiso  17878  mhmid  18978  mhmmnd  18979  ghmgrp  18981  ghmcmn  19736  ablfac2  19996  ringinvnz1ne0  20184  rngqipring1  21154  zringlpirlem1  21312  mp2pm2mplem4  22621  neiptopuni  22944  neiptoptop  22945  neiptopnei  22946  neitr  22994  hauscmplem  23220  2ndcomap  23272  lly1stc  23310  dissnref  23342  neitx  23421  cnextcn  23881  ustexsym  24030  ustex2sym  24031  ustex3sym  24032  trust  24044  utoptop  24049  restutop  24052  restutopopn  24053  ustuqtop1  24056  ustuqtop2  24057  ustuqtop3  24058  ustuqtop4  24059  utopreg  24067  ucncn  24100  fmucnd  24107  cfilufg  24108  trcfilu  24109  neipcfilu  24111  metustid  24373  metustsym  24374  metustexhalf  24375  metust  24377  cfilucfil  24378  metustbl  24385  psmetutop  24386  restmetu  24389  qdensere  24596  opnreen  24657  nmoleub2lem3  24952  ovolicc2lem4  25359  plydivlem4  26138  ulmuni  26233  dchrpt  27104  tgcgrtriv  28159  tgbtwntriv2  28162  tgbtwncom  28163  tgbtwnswapid  28167  tgbtwnintr  28168  tgbtwnouttr2  28170  tgtrisegint  28174  tgifscgr  28183  tgcgrxfr  28193  tgbtwnxfr  28205  motcgrg  28219  tgbtwnconn1lem3  28249  tgbtwnconn1  28250  tgbtwnconn3  28252  legval  28259  legov  28260  legov2  28261  legtrd  28264  legtri3  28265  legtrid  28266  ltgseg  28271  hlcgrex  28291  hlcgreulem  28292  colline  28324  miriso  28345  symquadlem  28364  krippenlem  28365  midexlem  28367  perpneq  28389  isperp2  28390  footexALT  28393  footex  28396  perpdrag  28403  colperpexlem3  28407  colperpex  28408  opphllem  28410  mideulem  28411  midex  28412  oppne3  28418  oppnid  28421  opphllem3  28424  opphllem5  28426  opphllem6  28427  oppperpex  28428  opphl  28429  outpasch  28430  hpgne1  28436  hpgne2  28437  lnopp2hpgb  28438  colopp  28444  lmieu  28459  lnperpex  28478  trgcopy  28479  trgcopyeulem  28480  acopy  28508  acopyeu  28509  inaghl  28520  leagne1  28524  leagne2  28525  leagne3  28526  leagne4  28527  cgrg3col4  28528  tgasa1  28533  f1otrg  28546  ttgbtwnid  28565  cnvbraval  31787  opsqrlem1  31817  rabfodom  32167  acunirnmpt  32308  acunirnmpt2  32309  acunirnmpt2f  32310  xrge0infss  32397  fsumiunle  32459  wrdt2ind  32541  mgcf1o  32597  gsummpt2d  32628  trsp2cyc  32709  cycpmrn  32729  tocyccntz  32730  cyc3evpm  32736  cyc3genpm  32738  cycpmgcl  32739  cycpmconjslem2  32741  cyc3conja  32743  archirngz  32762  archiabllem1a  32764  archiabllem1b  32765  archiabllem1  32766  archiabllem2a  32767  archiabllem2c  32768  archiabl  32771  isdrng4  32822  imaslmod  32895  znfermltl  32910  nsgqusf1olem1  32955  ghmquskerlem3  32962  ghmqusker  32963  lmhmqusker  32965  unitpidl1  32973  rhmquskerlem  32974  rhmimaidl  32981  drngidl  32982  isprmidlc  32997  qsidomlem2  33003  mxidlprm  33017  mxidlirredi  33018  mxidlirred  33019  opprqusplusg  33034  opprqusmulr  33036  qsdrngi  33040  qsdrnglem2  33041  dimval  33130  dimvalfi  33131  lssdimle  33137  lbsdiflsp0  33156  dimkerim  33157  fedgmul  33161  extdg1id  33187  irngnminplynz  33217  txomap  33269  qtophaus  33271  pcmplfinf  33296  zarcls1  33304  zarclsun  33305  zarclsint  33307  zarclssn  33308  zarcmplem  33316  rhmpreimacn  33320  pstmxmet  33332  pnfneige0  33386  esumcst  33516  esum2d  33546  esumiun  33547  ddemeas  33689  signsply0  34017  signstres  34041  prodfzo03  34070  actfunsnf1o  34071  actfunsnrndisj  34072  tgoldbachgt  34130  poimirlem17  36961  poimirlem20  36964  itg2gt0cn  36999  fdc1  37070  lhprelat3N  39367  dihjat2  40758  aks4d1p8  41411  prjspersym  41804  eldioph2b  41956  diophrex  41968  irrapxlem6  42020  pellex  42028  pellfundex  42079  lnrfg  42316  mpaaeu  42347  cvgdvgrat  43527  climsuse  44775  limsupre  44808  limcleqr  44811  limsuppnfdlem  44868  limsupub2  44979  xlimclim2lem  45006  climxlim2  45013  cncficcgt0  45055  dvbdfbdioo  45097  ioodvbdlimc1lem2  45099  ioodvbdlimc2lem  45101  stoweidlem28  45195  stoweidlem29  45196  stoweidlem52  45219  stoweidlem60  45227  fourierdlem39  45313  fourierdlem102  45375  fourierdlem103  45376  fourierdlem104  45377  fourierdlem114  45387  hspmbllem2  45794  nnsum4primesevenALTV  46920