Theorem r19.29a 3158

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-rex 3067

This theorem is referenced by:  xpdifid  6167  fimaproj  8135  modmuladdnn0  13907  1arith  16890  prmgaplem5  17018  prmgapprmolem  17024  ffthiso  17912  mhmid  19013  mhmmnd  19014  ghmgrp  19016  ghmquskerlem3  19231  ghmqusker  19232  ghmcmn  19780  ablfac2  20040  ringinvnz1ne0  20230  rngqipring1  21200  zringlpirlem1  21382  mp2pm2mplem4  22705  neiptopuni  23028  neiptoptop  23029  neiptopnei  23030  neitr  23078  hauscmplem  23304  2ndcomap  23356  lly1stc  23394  dissnref  23426  neitx  23505  cnextcn  23965  ustexsym  24114  ustex2sym  24115  ustex3sym  24116  trust  24128  utoptop  24133  restutop  24136  restutopopn  24137  ustuqtop1  24140  ustuqtop2  24141  ustuqtop3  24142  ustuqtop4  24143  utopreg  24151  ucncn  24184  fmucnd  24191  cfilufg  24192  trcfilu  24193  neipcfilu  24195  metustid  24457  metustsym  24458  metustexhalf  24459  metust  24461  cfilucfil  24462  metustbl  24469  psmetutop  24470  restmetu  24473  qdensere  24680  opnreen  24741  nmoleub2lem3  25036  ovolicc2lem4  25443  plydivlem4  26225  ulmuni  26322  dchrpt  27194  tgcgrtriv  28282  tgbtwntriv2  28285  tgbtwncom  28286  tgbtwnswapid  28290  tgbtwnintr  28291  tgbtwnouttr2  28293  tgtrisegint  28297  tgifscgr  28306  tgcgrxfr  28316  tgbtwnxfr  28328  motcgrg  28342  tgbtwnconn1lem3  28372  tgbtwnconn1  28373  tgbtwnconn3  28375  legval  28382  legov  28383  legov2  28384  legtrd  28387  legtri3  28388  legtrid  28389  ltgseg  28394  hlcgrex  28414  hlcgreulem  28415  colline  28447  miriso  28468  symquadlem  28487  krippenlem  28488  midexlem  28490  perpneq  28512  isperp2  28513  footexALT  28516  footex  28519  perpdrag  28526  colperpexlem3  28530  colperpex  28531  opphllem  28533  mideulem  28534  midex  28535  oppne3  28541  oppnid  28544  opphllem3  28547  opphllem5  28549  opphllem6  28550  oppperpex  28551  opphl  28552  outpasch  28553  hpgne1  28559  hpgne2  28560  lnopp2hpgb  28561  colopp  28567  lmieu  28582  lnperpex  28601  trgcopy  28602  trgcopyeulem  28603  acopy  28631  acopyeu  28632  inaghl  28643  leagne1  28647  leagne2  28648  leagne3  28649  leagne4  28650  cgrg3col4  28651  tgasa1  28656  f1otrg  28669  ttgbtwnid  28688  cnvbraval  31914  opsqrlem1  31944  rabfodom  32295  acunirnmpt  32439  acunirnmpt2  32440  acunirnmpt2f  32441  xrge0infss  32525  fsumiunle  32587  wrdt2ind  32669  mgcf1o  32725  gsummpt2d  32758  trsp2cyc  32839  cycpmrn  32859  tocyccntz  32860  cyc3evpm  32866  cyc3genpm  32868  cycpmgcl  32869  cycpmconjslem2  32871  cyc3conja  32873  archirngz  32892  archiabllem1a  32894  archiabllem1b  32895  archiabllem1  32896  archiabllem2a  32897  archiabllem2c  32898  archiabl  32901  isdrng4  32957  erler  32974  elrlocbasi  32975  rlocaddval  32977  rlocmulval  32978  rlocf1  32982  fracfld  32989  imaslmod  33060  znfermltl  33073  nsgqusf1olem1  33118  lmhmqusker  33122  ghmqusnsg  33126  unitpidl1  33134  rhmquskerlem  33135  rhmqusnsg  33138  rhmimaidl  33143  drngidl  33144  isprmidlc  33158  qsidomlem2  33164  mxidlprm  33178  mxidlirredi  33179  mxidlirred  33180  opprqusplusg  33195  opprqusmulr  33197  qsdrngi  33201  qsdrnglem2  33202  dimval  33289  dimvalfi  33290  lssdimle  33296  lbsdiflsp0  33315  dimkerim  33316  fedgmul  33320  extdg1id  33346  irngnminplynz  33377  txomap  33430  qtophaus  33432  pcmplfinf  33457  zarcls1  33465  zarclsun  33466  zarclsint  33468  zarclssn  33469  zarcmplem  33477  rhmpreimacn  33481  pstmxmet  33493  pnfneige0  33547  esumcst  33677  esum2d  33707  esumiun  33708  ddemeas  33850  signsply0  34178  signstres  34202  prodfzo03  34230  actfunsnf1o  34231  actfunsnrndisj  34232  tgoldbachgt  34290  poimirlem17  37105  poimirlem20  37108  itg2gt0cn  37143  fdc1  37214  lhprelat3N  39508  dihjat2  40899  aks4d1p8  41553  primrootspoweq0  41572  aks6d1c4  41590  aks6d1c6isolem1  41641  aks6d1c6isolem2  41642  aks6d1c6lem5  41644  prjspersym  42022  eldioph2b  42174  diophrex  42186  irrapxlem6  42238  pellex  42246  pellfundex  42297  lnrfg  42534  mpaaeu  42565  cvgdvgrat  43741  climsuse  44987  limsupre  45020  limcleqr  45023  limsuppnfdlem  45080  limsupub2  45191  xlimclim2lem  45218  climxlim2  45225  cncficcgt0  45267  dvbdfbdioo  45309  ioodvbdlimc1lem2  45311  ioodvbdlimc2lem  45313  stoweidlem28  45407  stoweidlem29  45408  stoweidlem52  45431  stoweidlem60  45439  fourierdlem39  45525  fourierdlem102  45587  fourierdlem103  45588  fourierdlem104  45589  fourierdlem114  45599  hspmbllem2  46006  nnsum4primesevenALTV  47132