Theorem r19.29a 3140

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  xpdifid  6115  fimaproj  8065  modmuladdnn0  13822  1arith  16839  prmgaplem5  16967  prmgapprmolem  16973  ffthiso  17838  chnso  18530  mhmid  18976  mhmmnd  18977  ghmgrp  18979  ghmqusnsg  19195  ghmquskerlem3  19199  ghmqusker  19200  ghmcmn  19744  ablfac2  20004  ringinvnz1ne0  20219  rhmqusnsg  21223  rngqipring1  21254  zringlpirlem1  21400  mp2pm2mplem4  22725  neiptopuni  23046  neiptoptop  23047  neiptopnei  23048  neitr  23096  hauscmplem  23322  2ndcomap  23374  lly1stc  23412  dissnref  23444  neitx  23523  cnextcn  23983  ustexsym  24132  ustex2sym  24133  ustex3sym  24134  trust  24145  utoptop  24150  restutop  24153  restutopopn  24154  ustuqtop1  24157  ustuqtop2  24158  ustuqtop3  24159  ustuqtop4  24160  utopreg  24168  ucncn  24200  fmucnd  24207  cfilufg  24208  trcfilu  24209  neipcfilu  24211  metustid  24470  metustsym  24471  metustexhalf  24472  metust  24474  cfilucfil  24475  metustbl  24482  psmetutop  24483  restmetu  24486  qdensere  24685  opnreen  24748  nmoleub2lem3  25043  ovolicc2lem4  25449  plydivlem4  26232  ulmuni  26329  dchrpt  27206  tgcgrtriv  28463  tgbtwntriv2  28466  tgbtwncom  28467  tgbtwnswapid  28471  tgbtwnintr  28472  tgbtwnouttr2  28474  tgtrisegint  28478  tgifscgr  28487  tgcgrxfr  28497  tgbtwnxfr  28509  motcgrg  28523  tgbtwnconn1lem3  28553  tgbtwnconn1  28554  tgbtwnconn3  28556  legval  28563  legov  28564  legov2  28565  legtrd  28568  legtri3  28569  legtrid  28570  ltgseg  28575  hlcgrex  28595  hlcgreulem  28596  colline  28628  miriso  28649  symquadlem  28668  krippenlem  28669  midexlem  28671  perpneq  28693  isperp2  28694  footexALT  28697  footex  28700  perpdrag  28707  colperpexlem3  28711  colperpex  28712  opphllem  28714  mideulem  28715  midex  28716  oppne3  28722  oppnid  28725  opphllem3  28728  opphllem5  28730  opphllem6  28731  oppperpex  28732  opphl  28733  outpasch  28734  hpgne1  28740  hpgne2  28741  lnopp2hpgb  28742  colopp  28748  lmieu  28763  lnperpex  28782  trgcopy  28783  trgcopyeulem  28784  acopy  28812  acopyeu  28813  inaghl  28824  leagne1  28828  leagne2  28829  leagne3  28830  leagne4  28831  cgrg3col4  28832  tgasa1  28837  f1otrg  28850  ttgbtwnid  28863  cnvbraval  32088  opsqrlem1  32118  rabfodom  32483  acunirnmpt  32639  acunirnmpt2  32640  acunirnmpt2f  32641  xrge0infss  32741  fsumiunle  32810  2exple2exp  32826  expevenpos  32827  wrdt2ind  32932  mgcf1o  32982  mndlactf1o  33009  gsummpt2d  33027  gsumwrd2dccatlem  33044  trsp2cyc  33090  cycpmrn  33110  tocyccntz  33111  cyc3evpm  33117  cyc3genpm  33119  cycpmgcl  33120  cycpmconjslem2  33122  cyc3conja  33124  archirngz  33156  archiabllem1a  33158  archiabllem1b  33159  archiabllem1  33160  archiabllem2a  33161  archiabllem2c  33162  archiabl  33165  elrgspnlem1  33207  elrgspnlem2  33208  elrgspnlem4  33210  elrgspnsubrunlem1  33212  elrgspnsubrunlem2  33213  elrgspnsubrun  33214  erler  33230  elrlocbasi  33231  rlocaddval  33233  rlocmulval  33234  rlocf1  33238  isdrng4  33259  fracfld  33272  imaslmod  33316  znfermltl  33329  nsgqusf1olem1  33376  lmhmqusker  33380  unitpidl1  33387  rhmquskerlem  33388  rhmimaidl  33395  drngidl  33396  isprmidlc  33410  qsidomlem2  33416  ssdifidlprm  33421  mxidlprm  33433  mxidlirredi  33434  mxidlirred  33435  drngmxidlr  33441  opprqusplusg  33452  opprqusmulr  33454  qsdrngi  33458  qsdrnglem2  33459  rprmasso2  33489  rprmirredlem  33493  1arithidom  33500  pidufd  33506  1arithufdlem1  33507  1arithufdlem2  33508  1arithufdlem3  33509  1arithufdlem4  33510  dfufd2lem  33512  dfufd2  33513  esplymhp  33587  esplyfv1  33588  esplyfv  33589  lbslelsp  33608  dimval  33611  dimvalfi  33612  lssdimle  33618  lbsdiflsp0  33637  dimkerim  33638  fedgmul  33642  dimlssid  33643  extdg1id  33677  fldextrspunlsplem  33684  extdgfialglem1  33703  extdgfialg  33705  irngnminplynz  33723  fldext2chn  33739  constrext2chnlem  33761  constrfiss  33762  constrllcllem  33763  constrlccllem  33764  constrcccllem  33765  constrcn  33771  cos9thpiminplylem2  33794  txomap  33845  qtophaus  33847  pcmplfinf  33872  zarcls1  33880  zarclsun  33881  zarclsint  33883  zarclssn  33884  zarcmplem  33892  rhmpreimacn  33896  pstmxmet  33908  pnfneige0  33962  esumcst  34074  esum2d  34104  esumiun  34105  ddemeas  34247  signsply0  34562  signstres  34586  prodfzo03  34614  actfunsnf1o  34615  actfunsnrndisj  34616  tgoldbachgt  34674  poimirlem17  37683  poimirlem20  37686  itg2gt0cn  37721  fdc1  37792  lhprelat3N  40085  dihjat2  41476  aks4d1p8  42126  primrootspoweq0  42145  aks6d1c4  42163  aks6d1c6isolem1  42213  aks6d1c6isolem2  42214  aks6d1c6lem5  42216  aks6d1c7  42223  rhmqusspan  42224  grpods  42233  unitscyglem1  42234  unitscyglem2  42235  unitscyglem3  42236  unitscyglem4  42237  aks5lem7  42239  aks5  42243  prjspersym  42646  eldioph2b  42802  diophrex  42814  irrapxlem6  42866  pellex  42874  pellfundex  42925  lnrfg  43158  mpaaeu  43189  cvgdvgrat  44352  climsuse  45654  limsupre  45685  limcleqr  45688  limsuppnfdlem  45745  liminflelimsuplem  45819  limsupub2  45856  xlimclim2lem  45883  climxlim2  45890  cncficcgt0  45932  dvbdfbdioo  45974  ioodvbdlimc1lem2  45976  ioodvbdlimc2lem  45978  stoweidlem28  46072  stoweidlem29  46073  stoweidlem52  46096  stoweidlem60  46104  fourierdlem39  46190  fourierdlem102  46252  fourierdlem103  46253  fourierdlem104  46254  fourierdlem114  46264  hspmbllem2  46671  nnsum4primesevenALTV  47838  imaf1co  49193