Theorem r19.29a 3151

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3060

This theorem is referenced by:  xpdifid  6174  fimaproj  8140  modmuladdnn0  13916  1arith  16899  prmgaplem5  17027  prmgapprmolem  17033  ffthiso  17921  mhmid  19027  mhmmnd  19028  ghmgrp  19030  ghmqusnsg  19245  ghmquskerlem3  19249  ghmqusker  19250  ghmcmn  19798  ablfac2  20058  ringinvnz1ne0  20248  rhmqusnsg  21192  rngqipring1  21223  zringlpirlem1  21405  mp2pm2mplem4  22755  neiptopuni  23078  neiptoptop  23079  neiptopnei  23080  neitr  23128  hauscmplem  23354  2ndcomap  23406  lly1stc  23444  dissnref  23476  neitx  23555  cnextcn  24015  ustexsym  24164  ustex2sym  24165  ustex3sym  24166  trust  24178  utoptop  24183  restutop  24186  restutopopn  24187  ustuqtop1  24190  ustuqtop2  24191  ustuqtop3  24192  ustuqtop4  24193  utopreg  24201  ucncn  24234  fmucnd  24241  cfilufg  24242  trcfilu  24243  neipcfilu  24245  metustid  24507  metustsym  24508  metustexhalf  24509  metust  24511  cfilucfil  24512  metustbl  24519  psmetutop  24520  restmetu  24523  qdensere  24730  opnreen  24791  nmoleub2lem3  25086  ovolicc2lem4  25493  plydivlem4  26276  ulmuni  26373  dchrpt  27245  tgcgrtriv  28360  tgbtwntriv2  28363  tgbtwncom  28364  tgbtwnswapid  28368  tgbtwnintr  28369  tgbtwnouttr2  28371  tgtrisegint  28375  tgifscgr  28384  tgcgrxfr  28394  tgbtwnxfr  28406  motcgrg  28420  tgbtwnconn1lem3  28450  tgbtwnconn1  28451  tgbtwnconn3  28453  legval  28460  legov  28461  legov2  28462  legtrd  28465  legtri3  28466  legtrid  28467  ltgseg  28472  hlcgrex  28492  hlcgreulem  28493  colline  28525  miriso  28546  symquadlem  28565  krippenlem  28566  midexlem  28568  perpneq  28590  isperp2  28591  footexALT  28594  footex  28597  perpdrag  28604  colperpexlem3  28608  colperpex  28609  opphllem  28611  mideulem  28612  midex  28613  oppne3  28619  oppnid  28622  opphllem3  28625  opphllem5  28627  opphllem6  28628  oppperpex  28629  opphl  28630  outpasch  28631  hpgne1  28637  hpgne2  28638  lnopp2hpgb  28639  colopp  28645  lmieu  28660  lnperpex  28679  trgcopy  28680  trgcopyeulem  28681  acopy  28709  acopyeu  28710  inaghl  28721  leagne1  28725  leagne2  28726  leagne3  28727  leagne4  28728  cgrg3col4  28729  tgasa1  28734  f1otrg  28747  ttgbtwnid  28766  cnvbraval  31992  opsqrlem1  32022  rabfodom  32379  acunirnmpt  32526  acunirnmpt2  32527  acunirnmpt2f  32528  xrge0infss  32612  fsumiunle  32677  wrdt2ind  32763  mgcf1o  32819  gsummpt2d  32853  trsp2cyc  32936  cycpmrn  32956  tocyccntz  32957  cyc3evpm  32963  cyc3genpm  32965  cycpmgcl  32966  cycpmconjslem2  32968  cyc3conja  32970  archirngz  32989  archiabllem1a  32991  archiabllem1b  32992  archiabllem1  32993  archiabllem2a  32994  archiabllem2c  32995  archiabl  32998  erler  33055  elrlocbasi  33056  rlocaddval  33058  rlocmulval  33059  rlocf1  33063  isdrng4  33083  fracfld  33094  imaslmod  33164  znfermltl  33177  nsgqusf1olem1  33225  lmhmqusker  33229  unitpidl1  33236  rhmquskerlem  33237  rhmimaidl  33244  drngidl  33245  isprmidlc  33259  qsidomlem2  33265  ssdifidlprm  33270  mxidlprm  33282  mxidlirredi  33283  mxidlirred  33284  drngmxidlr  33290  opprqusplusg  33301  opprqusmulr  33303  qsdrngi  33307  qsdrnglem2  33308  rprmasso2  33338  rprmirredlem  33342  1arithidom  33349  pidufd  33358  1arithufdlem1  33359  1arithufdlem2  33360  1arithufdlem3  33361  1arithufdlem4  33362  dfufd2lem  33364  dfufd2  33365  dimval  33429  dimvalfi  33430  lssdimle  33436  lbsdiflsp0  33455  dimkerim  33456  fedgmul  33460  extdg1id  33486  irngnminplynz  33513  txomap  33566  qtophaus  33568  pcmplfinf  33593  zarcls1  33601  zarclsun  33602  zarclsint  33604  zarclssn  33605  zarcmplem  33613  rhmpreimacn  33617  pstmxmet  33629  pnfneige0  33683  esumcst  33813  esum2d  33843  esumiun  33844  ddemeas  33986  signsply0  34314  signstres  34338  prodfzo03  34366  actfunsnf1o  34367  actfunsnrndisj  34368  tgoldbachgt  34426  poimirlem17  37241  poimirlem20  37244  itg2gt0cn  37279  fdc1  37350  lhprelat3N  39643  dihjat2  41034  aks4d1p8  41690  primrootspoweq0  41709  aks6d1c4  41727  aks6d1c6isolem1  41777  aks6d1c6isolem2  41778  aks6d1c6lem5  41780  aks6d1c7  41787  rhmqusspan  41788  prjspersym  42166  eldioph2b  42325  diophrex  42337  irrapxlem6  42389  pellex  42397  pellfundex  42448  lnrfg  42685  mpaaeu  42716  cvgdvgrat  43892  climsuse  45134  limsupre  45167  limcleqr  45170  limsuppnfdlem  45227  limsupub2  45338  xlimclim2lem  45365  climxlim2  45372  cncficcgt0  45414  dvbdfbdioo  45456  ioodvbdlimc1lem2  45458  ioodvbdlimc2lem  45460  stoweidlem28  45554  stoweidlem29  45555  stoweidlem52  45578  stoweidlem60  45586  fourierdlem39  45672  fourierdlem102  45734  fourierdlem103  45735  fourierdlem104  45736  fourierdlem114  45746  hspmbllem2  46153  nnsum4primesevenALTV  47278