Theorem r19.29a 3163

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  xpdifid  6168  fimaproj  8121  modmuladdnn0  13880  1arith  16860  prmgaplem5  16988  prmgapprmolem  16994  ffthiso  17880  mhmid  18946  mhmmnd  18947  ghmgrp  18949  ghmcmn  19699  ablfac2  19959  ringinvnz1ne0  20112  zringlpirlem1  21032  mp2pm2mplem4  22311  neiptopuni  22634  neiptoptop  22635  neiptopnei  22636  neitr  22684  hauscmplem  22910  2ndcomap  22962  lly1stc  23000  dissnref  23032  neitx  23111  cnextcn  23571  ustexsym  23720  ustex2sym  23721  ustex3sym  23722  trust  23734  utoptop  23739  restutop  23742  restutopopn  23743  ustuqtop1  23746  ustuqtop2  23747  ustuqtop3  23748  ustuqtop4  23749  utopreg  23757  ucncn  23790  fmucnd  23797  cfilufg  23798  trcfilu  23799  neipcfilu  23801  metustid  24063  metustsym  24064  metustexhalf  24065  metust  24067  cfilucfil  24068  metustbl  24075  psmetutop  24076  restmetu  24079  qdensere  24286  opnreen  24347  nmoleub2lem3  24631  ovolicc2lem4  25037  plydivlem4  25809  ulmuni  25904  dchrpt  26770  tgcgrtriv  27735  tgbtwntriv2  27738  tgbtwncom  27739  tgbtwnswapid  27743  tgbtwnintr  27744  tgbtwnouttr2  27746  tgtrisegint  27750  tgifscgr  27759  tgcgrxfr  27769  tgbtwnxfr  27781  motcgrg  27795  tgbtwnconn1lem3  27825  tgbtwnconn1  27826  tgbtwnconn3  27828  legval  27835  legov  27836  legov2  27837  legtrd  27840  legtri3  27841  legtrid  27842  ltgseg  27847  hlcgrex  27867  hlcgreulem  27868  colline  27900  miriso  27921  symquadlem  27940  krippenlem  27941  midexlem  27943  perpneq  27965  isperp2  27966  footexALT  27969  footex  27972  perpdrag  27979  colperpexlem3  27983  colperpex  27984  opphllem  27986  mideulem  27987  midex  27988  oppne3  27994  oppnid  27997  opphllem3  28000  opphllem5  28002  opphllem6  28003  oppperpex  28004  opphl  28005  outpasch  28006  hpgne1  28012  hpgne2  28013  lnopp2hpgb  28014  colopp  28020  lmieu  28035  lnperpex  28054  trgcopy  28055  trgcopyeulem  28056  acopy  28084  acopyeu  28085  inaghl  28096  leagne1  28100  leagne2  28101  leagne3  28102  leagne4  28103  cgrg3col4  28104  tgasa1  28109  f1otrg  28122  ttgbtwnid  28141  cnvbraval  31363  opsqrlem1  31393  rabfodom  31743  acunirnmpt  31884  acunirnmpt2  31885  acunirnmpt2f  31886  xrge0infss  31973  fsumiunle  32035  wrdt2ind  32117  mgcf1o  32173  gsummpt2d  32201  trsp2cyc  32282  cycpmrn  32302  tocyccntz  32303  cyc3evpm  32309  cyc3genpm  32311  cycpmgcl  32312  cycpmconjslem2  32314  cyc3conja  32316  archirngz  32335  archiabllem1a  32337  archiabllem1b  32338  archiabllem1  32339  archiabllem2a  32340  archiabllem2c  32341  archiabl  32344  isdrng4  32395  imaslmod  32468  znfermltl  32479  nsgqusf1olem1  32524  ghmquskerlem3  32531  ghmqusker  32532  lmhmqusker  32534  unitpidl1  32542  rhmquskerlem  32543  rhmimaidl  32550  drngidl  32551  isprmidlc  32566  qsidomlem2  32572  mxidlprm  32586  mxidlirredi  32587  mxidlirred  32588  opprqusplusg  32603  opprqusmulr  32605  qsdrngi  32609  qsdrnglem2  32610  dimval  32686  dimvalfi  32687  lssdimle  32692  lbsdiflsp0  32711  dimkerim  32712  fedgmul  32716  extdg1id  32742  irngnminplynz  32771  txomap  32814  qtophaus  32816  pcmplfinf  32841  zarcls1  32849  zarclsun  32850  zarclsint  32852  zarclssn  32853  zarcmplem  32861  rhmpreimacn  32865  pstmxmet  32877  pnfneige0  32931  esumcst  33061  esum2d  33091  esumiun  33092  ddemeas  33234  signsply0  33562  signstres  33586  prodfzo03  33615  actfunsnf1o  33616  actfunsnrndisj  33617  tgoldbachgt  33675  poimirlem17  36505  poimirlem20  36508  itg2gt0cn  36543  fdc1  36614  lhprelat3N  38911  dihjat2  40302  aks4d1p8  40952  prjspersym  41349  eldioph2b  41501  diophrex  41513  irrapxlem6  41565  pellex  41573  pellfundex  41624  lnrfg  41861  mpaaeu  41892  cvgdvgrat  43072  climsuse  44324  limsupre  44357  limcleqr  44360  limsuppnfdlem  44417  limsupub2  44528  xlimclim2lem  44555  climxlim2  44562  cncficcgt0  44604  dvbdfbdioo  44646  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  stoweidlem28  44744  stoweidlem29  44745  stoweidlem52  44768  stoweidlem60  44776  fourierdlem39  44862  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem114  44936  hspmbllem2  45343  nnsum4primesevenALTV  46469  rngqipring1  46801