Theorem r19.29a 3142

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 3137	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 15	1 ⊢ (𝜑 → 𝜒)

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

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 3055

This theorem is referenced by:  xpdifid  6143  fimaproj  8116  modmuladdnn0  13886  1arith  16904  prmgaplem5  17032  prmgapprmolem  17038  ffthiso  17899  mhmid  19001  mhmmnd  19002  ghmgrp  19004  ghmqusnsg  19220  ghmquskerlem3  19224  ghmqusker  19225  ghmcmn  19767  ablfac2  20027  ringinvnz1ne0  20215  rhmqusnsg  21201  rngqipring1  21232  zringlpirlem1  21378  mp2pm2mplem4  22702  neiptopuni  23023  neiptoptop  23024  neiptopnei  23025  neitr  23073  hauscmplem  23299  2ndcomap  23351  lly1stc  23389  dissnref  23421  neitx  23500  cnextcn  23960  ustexsym  24109  ustex2sym  24110  ustex3sym  24111  trust  24123  utoptop  24128  restutop  24131  restutopopn  24132  ustuqtop1  24135  ustuqtop2  24136  ustuqtop3  24137  ustuqtop4  24138  utopreg  24146  ucncn  24178  fmucnd  24185  cfilufg  24186  trcfilu  24187  neipcfilu  24189  metustid  24448  metustsym  24449  metustexhalf  24450  metust  24452  cfilucfil  24453  metustbl  24460  psmetutop  24461  restmetu  24464  qdensere  24663  opnreen  24726  nmoleub2lem3  25021  ovolicc2lem4  25427  plydivlem4  26210  ulmuni  26307  dchrpt  27184  tgcgrtriv  28417  tgbtwntriv2  28420  tgbtwncom  28421  tgbtwnswapid  28425  tgbtwnintr  28426  tgbtwnouttr2  28428  tgtrisegint  28432  tgifscgr  28441  tgcgrxfr  28451  tgbtwnxfr  28463  motcgrg  28477  tgbtwnconn1lem3  28507  tgbtwnconn1  28508  tgbtwnconn3  28510  legval  28517  legov  28518  legov2  28519  legtrd  28522  legtri3  28523  legtrid  28524  ltgseg  28529  hlcgrex  28549  hlcgreulem  28550  colline  28582  miriso  28603  symquadlem  28622  krippenlem  28623  midexlem  28625  perpneq  28647  isperp2  28648  footexALT  28651  footex  28654  perpdrag  28661  colperpexlem3  28665  colperpex  28666  opphllem  28668  mideulem  28669  midex  28670  oppne3  28676  oppnid  28679  opphllem3  28682  opphllem5  28684  opphllem6  28685  oppperpex  28686  opphl  28687  outpasch  28688  hpgne1  28694  hpgne2  28695  lnopp2hpgb  28696  colopp  28702  lmieu  28717  lnperpex  28736  trgcopy  28737  trgcopyeulem  28738  acopy  28766  acopyeu  28767  inaghl  28778  leagne1  28782  leagne2  28783  leagne3  28784  leagne4  28785  cgrg3col4  28786  tgasa1  28791  f1otrg  28804  ttgbtwnid  28817  cnvbraval  32045  opsqrlem1  32075  rabfodom  32440  acunirnmpt  32589  acunirnmpt2  32590  acunirnmpt2f  32591  xrge0infss  32689  fsumiunle  32760  2exple2exp  32776  expevenpos  32777  wrdt2ind  32881  mgcf1o  32935  chnso  32946  mndlactf1o  32977  gsummpt2d  32995  gsumwrd2dccatlem  33012  trsp2cyc  33086  cycpmrn  33106  tocyccntz  33107  cyc3evpm  33113  cyc3genpm  33115  cycpmgcl  33116  cycpmconjslem2  33118  cyc3conja  33120  archirngz  33149  archiabllem1a  33151  archiabllem1b  33152  archiabllem1  33153  archiabllem2a  33154  archiabllem2c  33155  archiabl  33158  elrgspnlem1  33199  elrgspnlem2  33200  elrgspnlem4  33202  elrgspnsubrunlem1  33204  elrgspnsubrunlem2  33205  elrgspnsubrun  33206  erler  33222  elrlocbasi  33223  rlocaddval  33225  rlocmulval  33226  rlocf1  33230  isdrng4  33251  fracfld  33264  imaslmod  33330  znfermltl  33343  nsgqusf1olem1  33390  lmhmqusker  33394  unitpidl1  33401  rhmquskerlem  33402  rhmimaidl  33409  drngidl  33410  isprmidlc  33424  qsidomlem2  33430  ssdifidlprm  33435  mxidlprm  33447  mxidlirredi  33448  mxidlirred  33449  drngmxidlr  33455  opprqusplusg  33466  opprqusmulr  33468  qsdrngi  33472  qsdrnglem2  33473  rprmasso2  33503  rprmirredlem  33507  1arithidom  33514  pidufd  33520  1arithufdlem1  33521  1arithufdlem2  33522  1arithufdlem3  33523  1arithufdlem4  33524  dfufd2lem  33526  dfufd2  33527  lbslelsp  33599  dimval  33602  dimvalfi  33603  lssdimle  33609  lbsdiflsp0  33628  dimkerim  33629  fedgmul  33633  dimlssid  33634  extdg1id  33667  fldextrspunlsplem  33674  irngnminplynz  33708  fldext2chn  33724  constrext2chnlem  33746  constrfiss  33747  constrllcllem  33748  constrlccllem  33749  constrcccllem  33750  constrcn  33756  cos9thpiminplylem2  33779  txomap  33830  qtophaus  33832  pcmplfinf  33857  zarcls1  33865  zarclsun  33866  zarclsint  33868  zarclssn  33869  zarcmplem  33877  rhmpreimacn  33881  pstmxmet  33893  pnfneige0  33947  esumcst  34059  esum2d  34089  esumiun  34090  ddemeas  34232  signsply0  34548  signstres  34572  prodfzo03  34600  actfunsnf1o  34601  actfunsnrndisj  34602  tgoldbachgt  34660  poimirlem17  37626  poimirlem20  37629  itg2gt0cn  37664  fdc1  37735  lhprelat3N  40029  dihjat2  41420  aks4d1p8  42070  primrootspoweq0  42089  aks6d1c4  42107  aks6d1c6isolem1  42157  aks6d1c6isolem2  42158  aks6d1c6lem5  42160  aks6d1c7  42167  rhmqusspan  42168  grpods  42177  unitscyglem1  42178  unitscyglem2  42179  unitscyglem3  42180  unitscyglem4  42181  aks5lem7  42183  aks5  42187  prjspersym  42588  eldioph2b  42744  diophrex  42756  irrapxlem6  42808  pellex  42816  pellfundex  42867  lnrfg  43101  mpaaeu  43132  cvgdvgrat  44295  climsuse  45599  limsupre  45632  limcleqr  45635  limsuppnfdlem  45692  liminflelimsuplem  45766  limsupub2  45803  xlimclim2lem  45830  climxlim2  45837  cncficcgt0  45879  dvbdfbdioo  45921  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  stoweidlem28  46019  stoweidlem29  46020  stoweidlem52  46043  stoweidlem60  46051  fourierdlem39  46137  fourierdlem102  46199  fourierdlem103  46200  fourierdlem104  46201  fourierdlem114  46211  hspmbllem2  46618  nnsum4primesevenALTV  47792  imaf1co  49131