Theorem r19.29a 3154

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098  ∃wrex 3062

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 396  df-ex 1774  df-rex 3063

This theorem is referenced by:  xpdifid  6158  fimaproj  8116  modmuladdnn0  13878  1arith  16861  prmgaplem5  16989  prmgapprmolem  16995  ffthiso  17883  mhmid  18983  mhmmnd  18984  ghmgrp  18986  ghmcmn  19743  ablfac2  20003  ringinvnz1ne0  20191  rngqipring1  21161  zringlpirlem1  21319  mp2pm2mplem4  22635  neiptopuni  22958  neiptoptop  22959  neiptopnei  22960  neitr  23008  hauscmplem  23234  2ndcomap  23286  lly1stc  23324  dissnref  23356  neitx  23435  cnextcn  23895  ustexsym  24044  ustex2sym  24045  ustex3sym  24046  trust  24058  utoptop  24063  restutop  24066  restutopopn  24067  ustuqtop1  24070  ustuqtop2  24071  ustuqtop3  24072  ustuqtop4  24073  utopreg  24081  ucncn  24114  fmucnd  24121  cfilufg  24122  trcfilu  24123  neipcfilu  24125  metustid  24387  metustsym  24388  metustexhalf  24389  metust  24391  cfilucfil  24392  metustbl  24399  psmetutop  24400  restmetu  24403  qdensere  24610  opnreen  24671  nmoleub2lem3  24966  ovolicc2lem4  25373  plydivlem4  26152  ulmuni  26247  dchrpt  27119  tgcgrtriv  28207  tgbtwntriv2  28210  tgbtwncom  28211  tgbtwnswapid  28215  tgbtwnintr  28216  tgbtwnouttr2  28218  tgtrisegint  28222  tgifscgr  28231  tgcgrxfr  28241  tgbtwnxfr  28253  motcgrg  28267  tgbtwnconn1lem3  28297  tgbtwnconn1  28298  tgbtwnconn3  28300  legval  28307  legov  28308  legov2  28309  legtrd  28312  legtri3  28313  legtrid  28314  ltgseg  28319  hlcgrex  28339  hlcgreulem  28340  colline  28372  miriso  28393  symquadlem  28412  krippenlem  28413  midexlem  28415  perpneq  28437  isperp2  28438  footexALT  28441  footex  28444  perpdrag  28451  colperpexlem3  28455  colperpex  28456  opphllem  28458  mideulem  28459  midex  28460  oppne3  28466  oppnid  28469  opphllem3  28472  opphllem5  28474  opphllem6  28475  oppperpex  28476  opphl  28477  outpasch  28478  hpgne1  28484  hpgne2  28485  lnopp2hpgb  28486  colopp  28492  lmieu  28507  lnperpex  28526  trgcopy  28527  trgcopyeulem  28528  acopy  28556  acopyeu  28557  inaghl  28568  leagne1  28572  leagne2  28573  leagne3  28574  leagne4  28575  cgrg3col4  28576  tgasa1  28581  f1otrg  28594  ttgbtwnid  28613  cnvbraval  31835  opsqrlem1  31865  rabfodom  32215  acunirnmpt  32356  acunirnmpt2  32357  acunirnmpt2f  32358  xrge0infss  32445  fsumiunle  32505  wrdt2ind  32587  mgcf1o  32643  gsummpt2d  32672  trsp2cyc  32753  cycpmrn  32773  tocyccntz  32774  cyc3evpm  32780  cyc3genpm  32782  cycpmgcl  32783  cycpmconjslem2  32785  cyc3conja  32787  archirngz  32806  archiabllem1a  32808  archiabllem1b  32809  archiabllem1  32810  archiabllem2a  32811  archiabllem2c  32812  archiabl  32815  isdrng4  32864  imaslmod  32937  znfermltl  32951  nsgqusf1olem1  32996  ghmquskerlem3  33003  ghmqusker  33004  lmhmqusker  33006  unitpidl1  33014  rhmquskerlem  33015  rhmimaidl  33022  drngidl  33023  isprmidlc  33038  qsidomlem2  33044  mxidlprm  33058  mxidlirredi  33059  mxidlirred  33060  opprqusplusg  33075  opprqusmulr  33077  qsdrngi  33081  qsdrnglem2  33082  dimval  33167  dimvalfi  33168  lssdimle  33174  lbsdiflsp0  33193  dimkerim  33194  fedgmul  33198  extdg1id  33224  irngnminplynz  33254  txomap  33306  qtophaus  33308  pcmplfinf  33333  zarcls1  33341  zarclsun  33342  zarclsint  33344  zarclssn  33345  zarcmplem  33353  rhmpreimacn  33357  pstmxmet  33369  pnfneige0  33423  esumcst  33553  esum2d  33583  esumiun  33584  ddemeas  33726  signsply0  34054  signstres  34078  prodfzo03  34106  actfunsnf1o  34107  actfunsnrndisj  34108  tgoldbachgt  34166  poimirlem17  36999  poimirlem20  37002  itg2gt0cn  37037  fdc1  37108  lhprelat3N  39405  dihjat2  40796  aks4d1p8  41449  prjspersym  41863  eldioph2b  42015  diophrex  42027  irrapxlem6  42079  pellex  42087  pellfundex  42138  lnrfg  42375  mpaaeu  42406  cvgdvgrat  43586  climsuse  44834  limsupre  44867  limcleqr  44870  limsuppnfdlem  44927  limsupub2  45038  xlimclim2lem  45065  climxlim2  45072  cncficcgt0  45114  dvbdfbdioo  45156  ioodvbdlimc1lem2  45158  ioodvbdlimc2lem  45160  stoweidlem28  45254  stoweidlem29  45255  stoweidlem52  45278  stoweidlem60  45286  fourierdlem39  45372  fourierdlem102  45434  fourierdlem103  45435  fourierdlem104  45436  fourierdlem114  45446  hspmbllem2  45853  nnsum4primesevenALTV  46979