Theorem r19.29a 3168

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  xpdifid  6199  fimaproj  8176  modmuladdnn0  13966  1arith  16974  prmgaplem5  17102  prmgapprmolem  17108  ffthiso  17996  mhmid  19103  mhmmnd  19104  ghmgrp  19106  ghmqusnsg  19322  ghmquskerlem3  19326  ghmqusker  19327  ghmcmn  19873  ablfac2  20133  ringinvnz1ne0  20323  rhmqusnsg  21318  rngqipring1  21349  zringlpirlem1  21496  mp2pm2mplem4  22836  neiptopuni  23159  neiptoptop  23160  neiptopnei  23161  neitr  23209  hauscmplem  23435  2ndcomap  23487  lly1stc  23525  dissnref  23557  neitx  23636  cnextcn  24096  ustexsym  24245  ustex2sym  24246  ustex3sym  24247  trust  24259  utoptop  24264  restutop  24267  restutopopn  24268  ustuqtop1  24271  ustuqtop2  24272  ustuqtop3  24273  ustuqtop4  24274  utopreg  24282  ucncn  24315  fmucnd  24322  cfilufg  24323  trcfilu  24324  neipcfilu  24326  metustid  24588  metustsym  24589  metustexhalf  24590  metust  24592  cfilucfil  24593  metustbl  24600  psmetutop  24601  restmetu  24604  qdensere  24811  opnreen  24872  nmoleub2lem3  25167  ovolicc2lem4  25574  plydivlem4  26356  ulmuni  26453  dchrpt  27329  tgcgrtriv  28510  tgbtwntriv2  28513  tgbtwncom  28514  tgbtwnswapid  28518  tgbtwnintr  28519  tgbtwnouttr2  28521  tgtrisegint  28525  tgifscgr  28534  tgcgrxfr  28544  tgbtwnxfr  28556  motcgrg  28570  tgbtwnconn1lem3  28600  tgbtwnconn1  28601  tgbtwnconn3  28603  legval  28610  legov  28611  legov2  28612  legtrd  28615  legtri3  28616  legtrid  28617  ltgseg  28622  hlcgrex  28642  hlcgreulem  28643  colline  28675  miriso  28696  symquadlem  28715  krippenlem  28716  midexlem  28718  perpneq  28740  isperp2  28741  footexALT  28744  footex  28747  perpdrag  28754  colperpexlem3  28758  colperpex  28759  opphllem  28761  mideulem  28762  midex  28763  oppne3  28769  oppnid  28772  opphllem3  28775  opphllem5  28777  opphllem6  28778  oppperpex  28779  opphl  28780  outpasch  28781  hpgne1  28787  hpgne2  28788  lnopp2hpgb  28789  colopp  28795  lmieu  28810  lnperpex  28829  trgcopy  28830  trgcopyeulem  28831  acopy  28859  acopyeu  28860  inaghl  28871  leagne1  28875  leagne2  28876  leagne3  28877  leagne4  28878  cgrg3col4  28879  tgasa1  28884  f1otrg  28897  ttgbtwnid  28916  cnvbraval  32142  opsqrlem1  32172  rabfodom  32533  acunirnmpt  32677  acunirnmpt2  32678  acunirnmpt2f  32679  xrge0infss  32767  fsumiunle  32833  wrdt2ind  32920  mgcf1o  32976  chnso  32986  mndlactf1o  33016  gsummpt2d  33032  trsp2cyc  33116  cycpmrn  33136  tocyccntz  33137  cyc3evpm  33143  cyc3genpm  33145  cycpmgcl  33146  cycpmconjslem2  33148  cyc3conja  33150  archirngz  33169  archiabllem1a  33171  archiabllem1b  33172  archiabllem1  33173  archiabllem2a  33174  archiabllem2c  33175  archiabl  33178  erler  33237  elrlocbasi  33238  rlocaddval  33240  rlocmulval  33241  rlocf1  33245  isdrng4  33264  fracfld  33275  imaslmod  33346  znfermltl  33359  nsgqusf1olem1  33406  lmhmqusker  33410  unitpidl1  33417  rhmquskerlem  33418  rhmimaidl  33425  drngidl  33426  isprmidlc  33440  qsidomlem2  33446  ssdifidlprm  33451  mxidlprm  33463  mxidlirredi  33464  mxidlirred  33465  drngmxidlr  33471  opprqusplusg  33482  opprqusmulr  33484  qsdrngi  33488  qsdrnglem2  33489  rprmasso2  33519  rprmirredlem  33523  1arithidom  33530  pidufd  33536  1arithufdlem1  33537  1arithufdlem2  33538  1arithufdlem3  33539  1arithufdlem4  33540  dfufd2lem  33542  dfufd2  33543  dimval  33613  dimvalfi  33614  lssdimle  33620  lbsdiflsp0  33639  dimkerim  33640  fedgmul  33644  dimlssid  33645  extdg1id  33676  irngnminplynz  33705  fldext2chn  33719  txomap  33780  qtophaus  33782  pcmplfinf  33807  zarcls1  33815  zarclsun  33816  zarclsint  33818  zarclssn  33819  zarcmplem  33827  rhmpreimacn  33831  pstmxmet  33843  pnfneige0  33897  esumcst  34027  esum2d  34057  esumiun  34058  ddemeas  34200  signsply0  34528  signstres  34552  prodfzo03  34580  actfunsnf1o  34581  actfunsnrndisj  34582  tgoldbachgt  34640  poimirlem17  37597  poimirlem20  37600  itg2gt0cn  37635  fdc1  37706  lhprelat3N  39997  dihjat2  41388  aks4d1p8  42044  primrootspoweq0  42063  aks6d1c4  42081  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  aks6d1c6lem5  42134  aks6d1c7  42141  rhmqusspan  42142  grpods  42151  unitscyglem1  42152  unitscyglem2  42153  unitscyglem3  42154  unitscyglem4  42155  aks5lem7  42157  aks5  42161  prjspersym  42562  eldioph2b  42719  diophrex  42731  irrapxlem6  42783  pellex  42791  pellfundex  42842  lnrfg  43076  mpaaeu  43107  cvgdvgrat  44282  climsuse  45529  limsupre  45562  limcleqr  45565  limsuppnfdlem  45622  limsupub2  45733  xlimclim2lem  45760  climxlim2  45767  cncficcgt0  45809  dvbdfbdioo  45851  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweidlem28  45949  stoweidlem29  45950  stoweidlem52  45973  stoweidlem60  45981  fourierdlem39  46067  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem114  46141  hspmbllem2  46548  nnsum4primesevenALTV  47675