Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.29a Structured version   Visualization version   GIF version

Theorem r19.29a 3282
 Description: A commonly used pattern in the spirit of r19.29 3249. (Contributed by Thierry Arnoux, 22-Nov-2017.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.)
Hypotheses
Ref Expression
rexlimdva2.1 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
r19.29a.1 (𝜑 → ∃𝑥𝐴 𝜓)
Assertion
Ref Expression
r19.29a (𝜑𝜒)
Distinct variable groups:   𝜒,𝑥   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.29a
StepHypRef Expression
1 r19.29a.1 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
2 rexlimdva2.1 . . 3 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
32rexlimdva2 3280 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 15 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2115  ∃wrex 3134 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 1912 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3138  df-rex 3139 This theorem is referenced by:  xpdifid  6012  fimaproj  7819  modmuladdnn0  13283  1arith  16257  prmgaplem5  16385  prmgapprmolem  16391  ffthiso  17195  mhmid  18216  mhmmnd  18217  ghmgrp  18219  ghmcmn  18948  ablfac2  19207  ringinvnz1ne0  19338  zringlpirlem1  20624  mp2pm2mplem4  21410  neiptopuni  21731  neiptoptop  21732  neiptopnei  21733  neitr  21781  hauscmplem  22007  2ndcomap  22059  lly1stc  22097  dissnref  22129  neitx  22208  cnextcn  22668  ustexsym  22817  ustex2sym  22818  ustex3sym  22819  trust  22831  utoptop  22836  restutop  22839  restutopopn  22840  ustuqtop1  22843  ustuqtop2  22844  ustuqtop3  22845  ustuqtop4  22846  utopreg  22854  ucncn  22887  fmucnd  22894  cfilufg  22895  trcfilu  22896  neipcfilu  22898  metustid  23157  metustsym  23158  metustexhalf  23159  metust  23161  cfilucfil  23162  metustbl  23169  psmetutop  23170  restmetu  23173  qdensere  23371  opnreen  23432  nmoleub2lem3  23716  ovolicc2lem4  24120  plydivlem4  24888  ulmuni  24983  dchrpt  25847  tgcgrtriv  26274  tgbtwntriv2  26277  tgbtwncom  26278  tgbtwnswapid  26282  tgbtwnintr  26283  tgbtwnouttr2  26285  tgtrisegint  26289  tgifscgr  26298  tgcgrxfr  26308  tgbtwnxfr  26320  motcgrg  26334  tgbtwnconn1lem3  26364  tgbtwnconn1  26365  tgbtwnconn3  26367  legval  26374  legov  26375  legov2  26376  legtrd  26379  legtri3  26380  legtrid  26381  ltgseg  26386  hlcgrex  26406  hlcgreulem  26407  colline  26439  miriso  26460  symquadlem  26479  krippenlem  26480  midexlem  26482  perpneq  26504  isperp2  26505  footexALT  26508  footex  26511  perpdrag  26518  colperpexlem3  26522  colperpex  26523  opphllem  26525  mideulem  26526  midex  26527  oppne3  26533  oppnid  26536  opphllem3  26539  opphllem5  26541  opphllem6  26542  oppperpex  26543  opphl  26544  outpasch  26545  hpgne1  26551  hpgne2  26552  lnopp2hpgb  26553  colopp  26559  lmieu  26574  lnperpex  26593  trgcopy  26594  trgcopyeulem  26595  acopy  26623  acopyeu  26624  inaghl  26635  leagne1  26639  leagne2  26640  leagne3  26641  leagne4  26642  cgrg3col4  26643  tgasa1  26648  f1otrg  26661  ttgbtwnid  26674  cnvbraval  29889  opsqrlem1  29919  rabfodom  30269  acunirnmpt  30408  acunirnmpt2  30409  acunirnmpt2f  30410  xrge0infss  30488  fsumiunle  30549  wrdt2ind  30631  gsummpt2d  30712  trsp2cyc  30790  cycpmrn  30810  tocyccntz  30811  cyc3evpm  30817  cyc3genpm  30819  cycpmgcl  30820  cycpmconjslem2  30822  cyc3conja  30824  archirngz  30843  archiabllem1a  30845  archiabllem1b  30846  archiabllem1  30847  archiabllem2a  30848  archiabllem2c  30849  archiabl  30852  imaslmod  30947  isprmidlc  30991  qsidomlem2  30994  mxidlprm  31005  dimval  31029  dimvalfi  31030  lssdimle  31034  lbsdiflsp0  31050  dimkerim  31051  fedgmul  31055  extdg1id  31081  txomap  31126  qtophaus  31128  pcmplfinf  31153  pstmxmet  31165  pnfneige0  31219  esumcst  31347  esum2d  31377  esumiun  31378  ddemeas  31520  signsply0  31846  signstres  31870  prodfzo03  31899  actfunsnf1o  31900  actfunsnrndisj  31901  tgoldbachgt  31959  poimirlem17  34984  poimirlem20  34987  itg2gt0cn  35022  fdc1  35094  lhprelat3N  37246  dihjat2  38637  prjspersym  39454  eldioph2b  39557  diophrex  39569  irrapxlem6  39621  pellex  39629  pellfundex  39680  lnrfg  39916  mpaaeu  39947  cvgdvgrat  40874  climsuse  42113  limsupre  42146  limcleqr  42149  limsuppnfdlem  42206  limsupub2  42317  xlimclim2lem  42344  climxlim2  42351  cncficcgt0  42393  dvbdfbdioo  42435  ioodvbdlimc1lem2  42437  ioodvbdlimc2lem  42439  stoweidlem28  42533  stoweidlem29  42534  stoweidlem52  42557  stoweidlem60  42565  fourierdlem39  42651  fourierdlem102  42713  fourierdlem103  42714  fourierdlem104  42715  fourierdlem114  42725  hspmbllem2  43129  nnsum4primesevenALTV  44182
 Copyright terms: Public domain W3C validator