Theorem r19.29a 3149

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3062

This theorem is referenced by:  xpdifid  6162  fimaproj  8139  modmuladdnn0  13938  1arith  16952  prmgaplem5  17080  prmgapprmolem  17086  ffthiso  17949  mhmid  19051  mhmmnd  19052  ghmgrp  19054  ghmqusnsg  19270  ghmquskerlem3  19274  ghmqusker  19275  ghmcmn  19817  ablfac2  20077  ringinvnz1ne0  20265  rhmqusnsg  21251  rngqipring1  21282  zringlpirlem1  21428  mp2pm2mplem4  22752  neiptopuni  23073  neiptoptop  23074  neiptopnei  23075  neitr  23123  hauscmplem  23349  2ndcomap  23401  lly1stc  23439  dissnref  23471  neitx  23550  cnextcn  24010  ustexsym  24159  ustex2sym  24160  ustex3sym  24161  trust  24173  utoptop  24178  restutop  24181  restutopopn  24182  ustuqtop1  24185  ustuqtop2  24186  ustuqtop3  24187  ustuqtop4  24188  utopreg  24196  ucncn  24228  fmucnd  24235  cfilufg  24236  trcfilu  24237  neipcfilu  24239  metustid  24498  metustsym  24499  metustexhalf  24500  metust  24502  cfilucfil  24503  metustbl  24510  psmetutop  24511  restmetu  24514  qdensere  24713  opnreen  24776  nmoleub2lem3  25071  ovolicc2lem4  25478  plydivlem4  26261  ulmuni  26358  dchrpt  27235  tgcgrtriv  28468  tgbtwntriv2  28471  tgbtwncom  28472  tgbtwnswapid  28476  tgbtwnintr  28477  tgbtwnouttr2  28479  tgtrisegint  28483  tgifscgr  28492  tgcgrxfr  28502  tgbtwnxfr  28514  motcgrg  28528  tgbtwnconn1lem3  28558  tgbtwnconn1  28559  tgbtwnconn3  28561  legval  28568  legov  28569  legov2  28570  legtrd  28573  legtri3  28574  legtrid  28575  ltgseg  28580  hlcgrex  28600  hlcgreulem  28601  colline  28633  miriso  28654  symquadlem  28673  krippenlem  28674  midexlem  28676  perpneq  28698  isperp2  28699  footexALT  28702  footex  28705  perpdrag  28712  colperpexlem3  28716  colperpex  28717  opphllem  28719  mideulem  28720  midex  28721  oppne3  28727  oppnid  28730  opphllem3  28733  opphllem5  28735  opphllem6  28736  oppperpex  28737  opphl  28738  outpasch  28739  hpgne1  28745  hpgne2  28746  lnopp2hpgb  28747  colopp  28753  lmieu  28768  lnperpex  28787  trgcopy  28788  trgcopyeulem  28789  acopy  28817  acopyeu  28818  inaghl  28829  leagne1  28833  leagne2  28834  leagne3  28835  leagne4  28836  cgrg3col4  28837  tgasa1  28842  f1otrg  28855  ttgbtwnid  28868  cnvbraval  32096  opsqrlem1  32126  rabfodom  32491  acunirnmpt  32642  acunirnmpt2  32643  acunirnmpt2f  32644  xrge0infss  32742  fsumiunle  32813  2exple2exp  32829  expevenpos  32830  wrdt2ind  32934  mgcf1o  32988  chnso  32999  mndlactf1o  33030  gsummpt2d  33048  gsumwrd2dccatlem  33065  trsp2cyc  33139  cycpmrn  33159  tocyccntz  33160  cyc3evpm  33166  cyc3genpm  33168  cycpmgcl  33169  cycpmconjslem2  33171  cyc3conja  33173  archirngz  33192  archiabllem1a  33194  archiabllem1b  33195  archiabllem1  33196  archiabllem2a  33197  archiabllem2c  33198  archiabl  33201  elrgspnlem1  33242  elrgspnlem2  33243  elrgspnlem4  33245  elrgspnsubrunlem1  33247  elrgspnsubrunlem2  33248  elrgspnsubrun  33249  erler  33265  elrlocbasi  33266  rlocaddval  33268  rlocmulval  33269  rlocf1  33273  isdrng4  33294  fracfld  33307  imaslmod  33373  znfermltl  33386  nsgqusf1olem1  33433  lmhmqusker  33437  unitpidl1  33444  rhmquskerlem  33445  rhmimaidl  33452  drngidl  33453  isprmidlc  33467  qsidomlem2  33473  ssdifidlprm  33478  mxidlprm  33490  mxidlirredi  33491  mxidlirred  33492  drngmxidlr  33498  opprqusplusg  33509  opprqusmulr  33511  qsdrngi  33515  qsdrnglem2  33516  rprmasso2  33546  rprmirredlem  33550  1arithidom  33557  pidufd  33563  1arithufdlem1  33564  1arithufdlem2  33565  1arithufdlem3  33566  1arithufdlem4  33567  dfufd2lem  33569  dfufd2  33570  lbslelsp  33642  dimval  33645  dimvalfi  33646  lssdimle  33652  lbsdiflsp0  33671  dimkerim  33672  fedgmul  33676  dimlssid  33677  extdg1id  33712  fldextrspunlsplem  33719  irngnminplynz  33751  fldext2chn  33767  constrext2chnlem  33789  constrfiss  33790  constrllcllem  33791  constrlccllem  33792  constrcccllem  33793  constrcn  33799  cos9thpiminplylem2  33822  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  34588  signstres  34612  prodfzo03  34640  actfunsnf1o  34641  actfunsnrndisj  34642  tgoldbachgt  34700  poimirlem17  37666  poimirlem20  37669  itg2gt0cn  37704  fdc1  37775  lhprelat3N  40064  dihjat2  41455  aks4d1p8  42105  primrootspoweq0  42124  aks6d1c4  42142  aks6d1c6isolem1  42192  aks6d1c6isolem2  42193  aks6d1c6lem5  42195  aks6d1c7  42202  rhmqusspan  42203  grpods  42212  unitscyglem1  42213  unitscyglem2  42214  unitscyglem3  42215  unitscyglem4  42216  aks5lem7  42218  aks5  42222  prjspersym  42605  eldioph2b  42761  diophrex  42773  irrapxlem6  42825  pellex  42833  pellfundex  42884  lnrfg  43118  mpaaeu  43149  cvgdvgrat  44312  climsuse  45617  limsupre  45650  limcleqr  45653  limsuppnfdlem  45710  liminflelimsuplem  45784  limsupub2  45821  xlimclim2lem  45848  climxlim2  45855  cncficcgt0  45897  dvbdfbdioo  45939  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  stoweidlem28  46037  stoweidlem29  46038  stoweidlem52  46061  stoweidlem60  46069  fourierdlem39  46155  fourierdlem102  46217  fourierdlem103  46218  fourierdlem104  46219  fourierdlem114  46229  hspmbllem2  46636  nnsum4primesevenALTV  47795  imaf1co  49075