Theorem r19.29a 3162

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  xpdifid  6167  fimaproj  8120  modmuladdnn0  13879  1arith  16859  prmgaplem5  16987  prmgapprmolem  16993  ffthiso  17879  mhmid  18945  mhmmnd  18946  ghmgrp  18948  ghmcmn  19698  ablfac2  19958  ringinvnz1ne0  20111  zringlpirlem1  21031  mp2pm2mplem4  22310  neiptopuni  22633  neiptoptop  22634  neiptopnei  22635  neitr  22683  hauscmplem  22909  2ndcomap  22961  lly1stc  22999  dissnref  23031  neitx  23110  cnextcn  23570  ustexsym  23719  ustex2sym  23720  ustex3sym  23721  trust  23733  utoptop  23738  restutop  23741  restutopopn  23742  ustuqtop1  23745  ustuqtop2  23746  ustuqtop3  23747  ustuqtop4  23748  utopreg  23756  ucncn  23789  fmucnd  23796  cfilufg  23797  trcfilu  23798  neipcfilu  23800  metustid  24062  metustsym  24063  metustexhalf  24064  metust  24066  cfilucfil  24067  metustbl  24074  psmetutop  24075  restmetu  24078  qdensere  24285  opnreen  24346  nmoleub2lem3  24630  ovolicc2lem4  25036  plydivlem4  25808  ulmuni  25903  dchrpt  26767  tgcgrtriv  27732  tgbtwntriv2  27735  tgbtwncom  27736  tgbtwnswapid  27740  tgbtwnintr  27741  tgbtwnouttr2  27743  tgtrisegint  27747  tgifscgr  27756  tgcgrxfr  27766  tgbtwnxfr  27778  motcgrg  27792  tgbtwnconn1lem3  27822  tgbtwnconn1  27823  tgbtwnconn3  27825  legval  27832  legov  27833  legov2  27834  legtrd  27837  legtri3  27838  legtrid  27839  ltgseg  27844  hlcgrex  27864  hlcgreulem  27865  colline  27897  miriso  27918  symquadlem  27937  krippenlem  27938  midexlem  27940  perpneq  27962  isperp2  27963  footexALT  27966  footex  27969  perpdrag  27976  colperpexlem3  27980  colperpex  27981  opphllem  27983  mideulem  27984  midex  27985  oppne3  27991  oppnid  27994  opphllem3  27997  opphllem5  27999  opphllem6  28000  oppperpex  28001  opphl  28002  outpasch  28003  hpgne1  28009  hpgne2  28010  lnopp2hpgb  28011  colopp  28017  lmieu  28032  lnperpex  28051  trgcopy  28052  trgcopyeulem  28053  acopy  28081  acopyeu  28082  inaghl  28093  leagne1  28097  leagne2  28098  leagne3  28099  leagne4  28100  cgrg3col4  28101  tgasa1  28106  f1otrg  28119  ttgbtwnid  28138  cnvbraval  31358  opsqrlem1  31388  rabfodom  31738  acunirnmpt  31879  acunirnmpt2  31880  acunirnmpt2f  31881  xrge0infss  31968  fsumiunle  32030  wrdt2ind  32112  mgcf1o  32168  gsummpt2d  32196  trsp2cyc  32277  cycpmrn  32297  tocyccntz  32298  cyc3evpm  32304  cyc3genpm  32306  cycpmgcl  32307  cycpmconjslem2  32309  cyc3conja  32311  archirngz  32330  archiabllem1a  32332  archiabllem1b  32333  archiabllem1  32334  archiabllem2a  32335  archiabllem2c  32336  archiabl  32339  isdrng4  32390  imaslmod  32463  znfermltl  32474  nsgqusf1olem1  32519  ghmquskerlem3  32526  ghmqusker  32527  lmhmqusker  32529  unitpidl1  32537  rhmquskerlem  32538  rhmimaidl  32545  drngidl  32546  isprmidlc  32561  qsidomlem2  32567  mxidlprm  32581  mxidlirredi  32582  mxidlirred  32583  opprqusplusg  32598  opprqusmulr  32600  qsdrngi  32604  qsdrnglem2  32605  dimval  32681  dimvalfi  32682  lssdimle  32687  lbsdiflsp0  32706  dimkerim  32707  fedgmul  32711  extdg1id  32737  irngnminplynz  32766  txomap  32809  qtophaus  32811  pcmplfinf  32836  zarcls1  32844  zarclsun  32845  zarclsint  32847  zarclssn  32848  zarcmplem  32856  rhmpreimacn  32860  pstmxmet  32872  pnfneige0  32926  esumcst  33056  esum2d  33086  esumiun  33087  ddemeas  33229  signsply0  33557  signstres  33581  prodfzo03  33610  actfunsnf1o  33611  actfunsnrndisj  33612  tgoldbachgt  33670  poimirlem17  36500  poimirlem20  36503  itg2gt0cn  36538  fdc1  36609  lhprelat3N  38906  dihjat2  40297  aks4d1p8  40947  prjspersym  41350  eldioph2b  41491  diophrex  41503  irrapxlem6  41555  pellex  41563  pellfundex  41614  lnrfg  41851  mpaaeu  41882  cvgdvgrat  43062  climsuse  44314  limsupre  44347  limcleqr  44350  limsuppnfdlem  44407  limsupub2  44518  xlimclim2lem  44545  climxlim2  44552  cncficcgt0  44594  dvbdfbdioo  44636  ioodvbdlimc1lem2  44638  ioodvbdlimc2lem  44640  stoweidlem28  44734  stoweidlem29  44735  stoweidlem52  44758  stoweidlem60  44766  fourierdlem39  44852  fourierdlem102  44914  fourierdlem103  44915  fourierdlem104  44916  fourierdlem114  44926  hspmbllem2  45333  nnsum4primesevenALTV  46459  rngqipring1  46791