Theorem r19.29a 3141

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  xpdifid  6141  fimaproj  8114  modmuladdnn0  13880  1arith  16898  prmgaplem5  17026  prmgapprmolem  17032  ffthiso  17893  mhmid  18995  mhmmnd  18996  ghmgrp  18998  ghmqusnsg  19214  ghmquskerlem3  19218  ghmqusker  19219  ghmcmn  19761  ablfac2  20021  ringinvnz1ne0  20209  rhmqusnsg  21195  rngqipring1  21226  zringlpirlem1  21372  mp2pm2mplem4  22696  neiptopuni  23017  neiptoptop  23018  neiptopnei  23019  neitr  23067  hauscmplem  23293  2ndcomap  23345  lly1stc  23383  dissnref  23415  neitx  23494  cnextcn  23954  ustexsym  24103  ustex2sym  24104  ustex3sym  24105  trust  24117  utoptop  24122  restutop  24125  restutopopn  24126  ustuqtop1  24129  ustuqtop2  24130  ustuqtop3  24131  ustuqtop4  24132  utopreg  24140  ucncn  24172  fmucnd  24179  cfilufg  24180  trcfilu  24181  neipcfilu  24183  metustid  24442  metustsym  24443  metustexhalf  24444  metust  24446  cfilucfil  24447  metustbl  24454  psmetutop  24455  restmetu  24458  qdensere  24657  opnreen  24720  nmoleub2lem3  25015  ovolicc2lem4  25421  plydivlem4  26204  ulmuni  26301  dchrpt  27178  tgcgrtriv  28411  tgbtwntriv2  28414  tgbtwncom  28415  tgbtwnswapid  28419  tgbtwnintr  28420  tgbtwnouttr2  28422  tgtrisegint  28426  tgifscgr  28435  tgcgrxfr  28445  tgbtwnxfr  28457  motcgrg  28471  tgbtwnconn1lem3  28501  tgbtwnconn1  28502  tgbtwnconn3  28504  legval  28511  legov  28512  legov2  28513  legtrd  28516  legtri3  28517  legtrid  28518  ltgseg  28523  hlcgrex  28543  hlcgreulem  28544  colline  28576  miriso  28597  symquadlem  28616  krippenlem  28617  midexlem  28619  perpneq  28641  isperp2  28642  footexALT  28645  footex  28648  perpdrag  28655  colperpexlem3  28659  colperpex  28660  opphllem  28662  mideulem  28663  midex  28664  oppne3  28670  oppnid  28673  opphllem3  28676  opphllem5  28678  opphllem6  28679  oppperpex  28680  opphl  28681  outpasch  28682  hpgne1  28688  hpgne2  28689  lnopp2hpgb  28690  colopp  28696  lmieu  28711  lnperpex  28730  trgcopy  28731  trgcopyeulem  28732  acopy  28760  acopyeu  28761  inaghl  28772  leagne1  28776  leagne2  28777  leagne3  28778  leagne4  28779  cgrg3col4  28780  tgasa1  28785  f1otrg  28798  ttgbtwnid  28811  cnvbraval  32039  opsqrlem1  32069  rabfodom  32434  acunirnmpt  32583  acunirnmpt2  32584  acunirnmpt2f  32585  xrge0infss  32683  fsumiunle  32754  2exple2exp  32770  expevenpos  32771  wrdt2ind  32875  mgcf1o  32929  chnso  32940  mndlactf1o  32971  gsummpt2d  32989  gsumwrd2dccatlem  33006  trsp2cyc  33080  cycpmrn  33100  tocyccntz  33101  cyc3evpm  33107  cyc3genpm  33109  cycpmgcl  33110  cycpmconjslem2  33112  cyc3conja  33114  archirngz  33143  archiabllem1a  33145  archiabllem1b  33146  archiabllem1  33147  archiabllem2a  33148  archiabllem2c  33149  archiabl  33152  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  elrgspnsubrun  33200  erler  33216  elrlocbasi  33217  rlocaddval  33219  rlocmulval  33220  rlocf1  33224  isdrng4  33245  fracfld  33258  imaslmod  33324  znfermltl  33337  nsgqusf1olem1  33384  lmhmqusker  33388  unitpidl1  33395  rhmquskerlem  33396  rhmimaidl  33403  drngidl  33404  isprmidlc  33418  qsidomlem2  33424  ssdifidlprm  33429  mxidlprm  33441  mxidlirredi  33442  mxidlirred  33443  drngmxidlr  33449  opprqusplusg  33460  opprqusmulr  33462  qsdrngi  33466  qsdrnglem2  33467  rprmasso2  33497  rprmirredlem  33501  1arithidom  33508  pidufd  33514  1arithufdlem1  33515  1arithufdlem2  33516  1arithufdlem3  33517  1arithufdlem4  33518  dfufd2lem  33520  dfufd2  33521  lbslelsp  33593  dimval  33596  dimvalfi  33597  lssdimle  33603  lbsdiflsp0  33622  dimkerim  33623  fedgmul  33627  dimlssid  33628  extdg1id  33661  fldextrspunlsplem  33668  irngnminplynz  33702  fldext2chn  33718  constrext2chnlem  33740  constrfiss  33741  constrllcllem  33742  constrlccllem  33743  constrcccllem  33744  constrcn  33750  cos9thpiminplylem2  33773  txomap  33824  qtophaus  33826  pcmplfinf  33851  zarcls1  33859  zarclsun  33860  zarclsint  33862  zarclssn  33863  zarcmplem  33871  rhmpreimacn  33875  pstmxmet  33887  pnfneige0  33941  esumcst  34053  esum2d  34083  esumiun  34084  ddemeas  34226  signsply0  34542  signstres  34566  prodfzo03  34594  actfunsnf1o  34595  actfunsnrndisj  34596  tgoldbachgt  34654  poimirlem17  37631  poimirlem20  37634  itg2gt0cn  37669  fdc1  37740  lhprelat3N  40034  dihjat2  41425  aks4d1p8  42075  primrootspoweq0  42094  aks6d1c4  42112  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  aks6d1c6lem5  42165  aks6d1c7  42172  rhmqusspan  42173  grpods  42182  unitscyglem1  42183  unitscyglem2  42184  unitscyglem3  42185  unitscyglem4  42186  aks5lem7  42188  aks5  42192  prjspersym  42595  eldioph2b  42751  diophrex  42763  irrapxlem6  42815  pellex  42823  pellfundex  42874  lnrfg  43108  mpaaeu  43139  cvgdvgrat  44302  climsuse  45606  limsupre  45639  limcleqr  45642  limsuppnfdlem  45699  liminflelimsuplem  45773  limsupub2  45810  xlimclim2lem  45837  climxlim2  45844  cncficcgt0  45886  dvbdfbdioo  45928  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem28  46026  stoweidlem29  46027  stoweidlem52  46050  stoweidlem60  46058  fourierdlem39  46144  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  hspmbllem2  46625  nnsum4primesevenALTV  47802  imaf1co  49144