Theorem r19.29a 3159

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  xpdifid  6189  fimaproj  8158  modmuladdnn0  13952  1arith  16960  prmgaplem5  17088  prmgapprmolem  17094  ffthiso  17982  mhmid  19093  mhmmnd  19094  ghmgrp  19096  ghmqusnsg  19312  ghmquskerlem3  19316  ghmqusker  19317  ghmcmn  19863  ablfac2  20123  ringinvnz1ne0  20313  rhmqusnsg  21312  rngqipring1  21343  zringlpirlem1  21490  mp2pm2mplem4  22830  neiptopuni  23153  neiptoptop  23154  neiptopnei  23155  neitr  23203  hauscmplem  23429  2ndcomap  23481  lly1stc  23519  dissnref  23551  neitx  23630  cnextcn  24090  ustexsym  24239  ustex2sym  24240  ustex3sym  24241  trust  24253  utoptop  24258  restutop  24261  restutopopn  24262  ustuqtop1  24265  ustuqtop2  24266  ustuqtop3  24267  ustuqtop4  24268  utopreg  24276  ucncn  24309  fmucnd  24316  cfilufg  24317  trcfilu  24318  neipcfilu  24320  metustid  24582  metustsym  24583  metustexhalf  24584  metust  24586  cfilucfil  24587  metustbl  24594  psmetutop  24595  restmetu  24598  qdensere  24805  opnreen  24866  nmoleub2lem3  25161  ovolicc2lem4  25568  plydivlem4  26352  ulmuni  26449  dchrpt  27325  tgcgrtriv  28506  tgbtwntriv2  28509  tgbtwncom  28510  tgbtwnswapid  28514  tgbtwnintr  28515  tgbtwnouttr2  28517  tgtrisegint  28521  tgifscgr  28530  tgcgrxfr  28540  tgbtwnxfr  28552  motcgrg  28566  tgbtwnconn1lem3  28596  tgbtwnconn1  28597  tgbtwnconn3  28599  legval  28606  legov  28607  legov2  28608  legtrd  28611  legtri3  28612  legtrid  28613  ltgseg  28618  hlcgrex  28638  hlcgreulem  28639  colline  28671  miriso  28692  symquadlem  28711  krippenlem  28712  midexlem  28714  perpneq  28736  isperp2  28737  footexALT  28740  footex  28743  perpdrag  28750  colperpexlem3  28754  colperpex  28755  opphllem  28757  mideulem  28758  midex  28759  oppne3  28765  oppnid  28768  opphllem3  28771  opphllem5  28773  opphllem6  28774  oppperpex  28775  opphl  28776  outpasch  28777  hpgne1  28783  hpgne2  28784  lnopp2hpgb  28785  colopp  28791  lmieu  28806  lnperpex  28825  trgcopy  28826  trgcopyeulem  28827  acopy  28855  acopyeu  28856  inaghl  28867  leagne1  28871  leagne2  28872  leagne3  28873  leagne4  28874  cgrg3col4  28875  tgasa1  28880  f1otrg  28893  ttgbtwnid  28912  cnvbraval  32138  opsqrlem1  32168  rabfodom  32532  acunirnmpt  32675  acunirnmpt2  32676  acunirnmpt2f  32677  xrge0infss  32770  fsumiunle  32835  wrdt2ind  32922  mgcf1o  32977  chnso  32987  mndlactf1o  33017  gsummpt2d  33034  gsumwrd2dccatlem  33051  trsp2cyc  33125  cycpmrn  33145  tocyccntz  33146  cyc3evpm  33152  cyc3genpm  33154  cycpmgcl  33155  cycpmconjslem2  33157  cyc3conja  33159  archirngz  33178  archiabllem1a  33180  archiabllem1b  33181  archiabllem1  33182  archiabllem2a  33183  archiabllem2c  33184  archiabl  33187  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem4  33234  erler  33251  elrlocbasi  33252  rlocaddval  33254  rlocmulval  33255  rlocf1  33259  isdrng4  33278  fracfld  33289  imaslmod  33360  znfermltl  33373  nsgqusf1olem1  33420  lmhmqusker  33424  unitpidl1  33431  rhmquskerlem  33432  rhmimaidl  33439  drngidl  33440  isprmidlc  33454  qsidomlem2  33460  ssdifidlprm  33465  mxidlprm  33477  mxidlirredi  33478  mxidlirred  33479  drngmxidlr  33485  opprqusplusg  33496  opprqusmulr  33498  qsdrngi  33502  qsdrnglem2  33503  rprmasso2  33533  rprmirredlem  33537  1arithidom  33544  pidufd  33550  1arithufdlem1  33551  1arithufdlem2  33552  1arithufdlem3  33553  1arithufdlem4  33554  dfufd2lem  33556  dfufd2  33557  dimval  33627  dimvalfi  33628  lssdimle  33634  lbsdiflsp0  33653  dimkerim  33654  fedgmul  33658  dimlssid  33659  extdg1id  33690  irngnminplynz  33719  fldext2chn  33733  txomap  33794  qtophaus  33796  pcmplfinf  33821  zarcls1  33829  zarclsun  33830  zarclsint  33832  zarclssn  33833  zarcmplem  33841  rhmpreimacn  33845  pstmxmet  33857  pnfneige0  33911  esumcst  34043  esum2d  34073  esumiun  34074  ddemeas  34216  signsply0  34544  signstres  34568  prodfzo03  34596  actfunsnf1o  34597  actfunsnrndisj  34598  tgoldbachgt  34656  poimirlem17  37623  poimirlem20  37626  itg2gt0cn  37661  fdc1  37732  lhprelat3N  40022  dihjat2  41413  aks4d1p8  42068  primrootspoweq0  42087  aks6d1c4  42105  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  aks6d1c6lem5  42158  aks6d1c7  42165  rhmqusspan  42166  grpods  42175  unitscyglem1  42176  unitscyglem2  42177  unitscyglem3  42178  unitscyglem4  42179  aks5lem7  42181  aks5  42185  prjspersym  42593  eldioph2b  42750  diophrex  42762  irrapxlem6  42814  pellex  42822  pellfundex  42873  lnrfg  43107  mpaaeu  43138  cvgdvgrat  44308  climsuse  45563  limsupre  45596  limcleqr  45599  limsuppnfdlem  45656  limsupub2  45767  xlimclim2lem  45794  climxlim2  45801  cncficcgt0  45843  dvbdfbdioo  45885  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweidlem28  45983  stoweidlem29  45984  stoweidlem52  46007  stoweidlem60  46015  fourierdlem39  46101  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  hspmbllem2  46582  nnsum4primesevenALTV  47725