Theorem r19.29a 3141

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  xpdifid  6122  fimaproj  8073  modmuladdnn0  13826  1arith  16843  prmgaplem5  16971  prmgapprmolem  16977  ffthiso  17842  chnso  18534  mhmid  18980  mhmmnd  18981  ghmgrp  18983  ghmqusnsg  19198  ghmquskerlem3  19202  ghmqusker  19203  ghmcmn  19747  ablfac2  20007  ringinvnz1ne0  20222  rhmqusnsg  21226  rngqipring1  21257  zringlpirlem1  21403  mp2pm2mplem4  22727  neiptopuni  23048  neiptoptop  23049  neiptopnei  23050  neitr  23098  hauscmplem  23324  2ndcomap  23376  lly1stc  23414  dissnref  23446  neitx  23525  cnextcn  23985  ustexsym  24134  ustex2sym  24135  ustex3sym  24136  trust  24147  utoptop  24152  restutop  24155  restutopopn  24156  ustuqtop1  24159  ustuqtop2  24160  ustuqtop3  24161  ustuqtop4  24162  utopreg  24170  ucncn  24202  fmucnd  24209  cfilufg  24210  trcfilu  24211  neipcfilu  24213  metustid  24472  metustsym  24473  metustexhalf  24474  metust  24476  cfilucfil  24477  metustbl  24484  psmetutop  24485  restmetu  24488  qdensere  24687  opnreen  24750  nmoleub2lem3  25045  ovolicc2lem4  25451  plydivlem4  26234  ulmuni  26331  dchrpt  27208  tgcgrtriv  28465  tgbtwntriv2  28468  tgbtwncom  28469  tgbtwnswapid  28473  tgbtwnintr  28474  tgbtwnouttr2  28476  tgtrisegint  28480  tgifscgr  28489  tgcgrxfr  28499  tgbtwnxfr  28511  motcgrg  28525  tgbtwnconn1lem3  28555  tgbtwnconn1  28556  tgbtwnconn3  28558  legval  28565  legov  28566  legov2  28567  legtrd  28570  legtri3  28571  legtrid  28572  ltgseg  28577  hlcgrex  28597  hlcgreulem  28598  colline  28630  miriso  28651  symquadlem  28670  krippenlem  28671  midexlem  28673  perpneq  28695  isperp2  28696  footexALT  28699  footex  28702  perpdrag  28709  colperpexlem3  28713  colperpex  28714  opphllem  28716  mideulem  28717  midex  28718  oppne3  28724  oppnid  28727  opphllem3  28730  opphllem5  28732  opphllem6  28733  oppperpex  28734  opphl  28735  outpasch  28736  hpgne1  28742  hpgne2  28743  lnopp2hpgb  28744  colopp  28750  lmieu  28765  lnperpex  28784  trgcopy  28785  trgcopyeulem  28786  acopy  28814  acopyeu  28815  inaghl  28826  leagne1  28830  leagne2  28831  leagne3  28832  leagne4  28833  cgrg3col4  28834  tgasa1  28839  f1otrg  28852  ttgbtwnid  28865  cnvbraval  32094  opsqrlem1  32124  rabfodom  32489  acunirnmpt  32645  acunirnmpt2  32646  acunirnmpt2f  32647  xrge0infss  32749  fsumiunle  32819  2exple2exp  32835  expevenpos  32836  wrdt2ind  32943  mgcf1o  32993  mndlactf1o  33020  gsummpt2d  33038  gsumwrd2dccatlem  33055  trsp2cyc  33101  cycpmrn  33121  tocyccntz  33122  cyc3evpm  33128  cyc3genpm  33130  cycpmgcl  33131  cycpmconjslem2  33133  cyc3conja  33135  archirngz  33167  archiabllem1a  33169  archiabllem1b  33170  archiabllem1  33171  archiabllem2a  33172  archiabllem2c  33173  archiabl  33176  elrgspnlem1  33218  elrgspnlem2  33219  elrgspnlem4  33221  elrgspnsubrunlem1  33223  elrgspnsubrunlem2  33224  elrgspnsubrun  33225  erler  33241  elrlocbasi  33242  rlocaddval  33244  rlocmulval  33245  rlocf1  33249  isdrng4  33270  fracfld  33283  imaslmod  33327  znfermltl  33340  nsgqusf1olem1  33387  lmhmqusker  33391  unitpidl1  33398  rhmquskerlem  33399  rhmimaidl  33406  drngidl  33407  isprmidlc  33421  qsidomlem2  33427  ssdifidlprm  33432  mxidlprm  33444  mxidlirredi  33445  mxidlirred  33446  drngmxidlr  33452  opprqusplusg  33463  opprqusmulr  33465  qsdrngi  33469  qsdrnglem2  33470  rprmasso2  33500  rprmirredlem  33504  1arithidom  33511  pidufd  33517  1arithufdlem1  33518  1arithufdlem2  33519  1arithufdlem3  33520  1arithufdlem4  33521  dfufd2lem  33523  dfufd2  33524  esplymhp  33610  esplyfv1  33611  esplyfv  33612  esplyfval3  33614  lbslelsp  33633  dimval  33636  dimvalfi  33637  lssdimle  33643  lbsdiflsp0  33662  dimkerim  33663  fedgmul  33667  dimlssid  33668  extdg1id  33702  fldextrspunlsplem  33709  extdgfialglem1  33728  extdgfialg  33730  irngnminplynz  33748  fldext2chn  33764  constrext2chnlem  33786  constrfiss  33787  constrllcllem  33788  constrlccllem  33789  constrcccllem  33790  constrcn  33796  cos9thpiminplylem2  33819  txomap  33870  qtophaus  33872  pcmplfinf  33897  zarcls1  33905  zarclsun  33906  zarclsint  33908  zarclssn  33909  zarcmplem  33917  rhmpreimacn  33921  pstmxmet  33933  pnfneige0  33987  esumcst  34099  esum2d  34129  esumiun  34130  ddemeas  34272  signsply0  34587  signstres  34611  prodfzo03  34639  actfunsnf1o  34640  actfunsnrndisj  34641  tgoldbachgt  34699  poimirlem17  37700  poimirlem20  37703  itg2gt0cn  37738  fdc1  37809  lhprelat3N  40162  dihjat2  41553  aks4d1p8  42203  primrootspoweq0  42222  aks6d1c4  42240  aks6d1c6isolem1  42290  aks6d1c6isolem2  42291  aks6d1c6lem5  42293  aks6d1c7  42300  rhmqusspan  42301  grpods  42310  unitscyglem1  42311  unitscyglem2  42312  unitscyglem3  42313  unitscyglem4  42314  aks5lem7  42316  aks5  42320  prjspersym  42728  eldioph2b  42883  diophrex  42895  irrapxlem6  42947  pellex  42955  pellfundex  43006  lnrfg  43239  mpaaeu  43270  cvgdvgrat  44433  climsuse  45735  limsupre  45766  limcleqr  45769  limsuppnfdlem  45826  liminflelimsuplem  45900  limsupub2  45937  xlimclim2lem  45964  climxlim2  45971  cncficcgt0  46013  dvbdfbdioo  46055  ioodvbdlimc1lem2  46057  ioodvbdlimc2lem  46059  stoweidlem28  46153  stoweidlem29  46154  stoweidlem52  46177  stoweidlem60  46185  fourierdlem39  46271  fourierdlem102  46333  fourierdlem103  46334  fourierdlem104  46335  fourierdlem114  46345  hspmbllem2  46752  nnsum4primesevenALTV  47928  imaf1co  49283