Theorem r19.29a 3148

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  xpdifid  6126  fimaproj  8082  modmuladdnn0  13875  1arith  16896  prmgaplem5  17024  prmgapprmolem  17030  ffthiso  17896  chnso  18588  mhmid  19037  mhmmnd  19038  ghmgrp  19040  ghmqusnsg  19255  ghmquskerlem3  19259  ghmqusker  19260  ghmcmn  19804  ablfac2  20064  ringinvnz1ne0  20279  rhmqusnsg  21285  rngqipring1  21316  zringlpirlem1  21444  mp2pm2mplem4  22799  neiptopuni  23120  neiptoptop  23121  neiptopnei  23122  neitr  23170  hauscmplem  23396  2ndcomap  23448  lly1stc  23486  dissnref  23518  neitx  23597  cnextcn  24057  ustexsym  24206  ustex2sym  24207  ustex3sym  24208  trust  24219  utoptop  24224  restutop  24227  restutopopn  24228  ustuqtop1  24231  ustuqtop2  24232  ustuqtop3  24233  ustuqtop4  24234  utopreg  24242  ucncn  24274  fmucnd  24281  cfilufg  24282  trcfilu  24283  neipcfilu  24285  metustid  24544  metustsym  24545  metustexhalf  24546  metust  24548  cfilucfil  24549  metustbl  24556  psmetutop  24557  restmetu  24560  qdensere  24759  opnreen  24822  nmoleub2lem3  25107  ovolicc2lem4  25512  plydivlem4  26287  ulmuni  26382  dchrpt  27255  tgcgrtriv  28577  tgbtwntriv2  28580  tgbtwncom  28581  tgbtwnswapid  28585  tgbtwnintr  28586  tgbtwnouttr2  28588  tgtrisegint  28592  tgifscgr  28601  tgcgrxfr  28611  tgbtwnxfr  28623  motcgrg  28637  tgbtwnconn1lem3  28667  tgbtwnconn1  28668  tgbtwnconn3  28670  legval  28677  legov  28678  legov2  28679  legtrd  28682  legtri3  28683  legtrid  28684  ltgseg  28689  hlcgrex  28709  hlcgreulem  28710  colline  28742  miriso  28763  symquadlem  28782  krippenlem  28783  midexlem  28785  perpneq  28807  isperp2  28808  footexALT  28811  footex  28814  perpdrag  28821  colperpexlem3  28825  colperpex  28826  opphllem  28828  mideulem  28829  midex  28830  oppne3  28836  oppnid  28839  opphllem3  28842  opphllem5  28844  opphllem6  28845  oppperpex  28846  opphl  28847  outpasch  28848  hpgne1  28854  hpgne2  28855  lnopp2hpgb  28856  colopp  28862  lmieu  28877  lnperpex  28896  trgcopy  28897  trgcopyeulem  28898  acopy  28926  acopyeu  28927  inaghl  28938  leagne1  28942  leagne2  28943  leagne3  28944  leagne4  28945  cgrg3col4  28946  tgasa1  28951  f1otrg  28964  ttgbtwnid  28977  cnvbraval  32206  opsqrlem1  32236  rabfodom  32600  acunirnmpt  32758  acunirnmpt2  32759  acunirnmpt2f  32760  xrge0infss  32859  fsumiunle  32928  2exple2exp  32944  expevenpos  32945  wrdt2ind  33039  mgcf1o  33089  mndlactf1o  33116  gsummpt2d  33137  gsumwrd2dccatlem  33165  trsp2cyc  33211  cycpmrn  33231  tocyccntz  33232  cyc3evpm  33238  cyc3genpm  33240  cycpmgcl  33241  cycpmconjslem2  33243  cyc3conja  33245  archirngz  33277  archiabllem1a  33279  archiabllem1b  33280  archiabllem1  33281  archiabllem2a  33282  archiabllem2c  33283  archiabl  33286  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem4  33333  elrgspnsubrunlem1  33335  elrgspnsubrunlem2  33336  elrgspnsubrun  33337  erler  33353  elrlocbasi  33354  rlocaddval  33356  rlocmulval  33357  rlocf1  33361  isdrng4  33386  fracfld  33399  imaslmod  33443  znfermltl  33456  nsgqusf1olem1  33503  lmhmqusker  33507  unitpidl1  33514  rhmquskerlem  33515  rhmimaidl  33522  drngidl  33523  isprmidlc  33537  qsidomlem2  33543  ssdifidlprm  33548  mxidlprm  33560  mxidlirredi  33561  mxidlirred  33562  drngmxidlr  33568  opprqusplusg  33579  opprqusmulr  33581  qsdrngi  33585  qsdrnglem2  33586  rprmasso2  33616  rprmirredlem  33620  1arithidom  33627  pidufd  33633  1arithufdlem1  33634  1arithufdlem2  33635  1arithufdlem3  33636  1arithufdlem4  33637  dfufd2lem  33639  dfufd2  33640  esplymhp  33759  esplyfv1  33760  esplyfv  33761  esplyfval3  33763  esplyfval1  33764  lbslelsp  33789  dimval  33792  dimvalfi  33793  lssdimle  33799  lbsdiflsp0  33817  dimkerim  33818  fedgmul  33822  dimlssid  33823  extdg1id  33857  fldextrspunlsplem  33864  extdgfialglem1  33883  extdgfialg  33885  irngnminplynz  33903  fldext2chn  33919  constrext2chnlem  33941  constrfiss  33942  constrllcllem  33943  constrlccllem  33944  constrcccllem  33945  constrcn  33951  cos9thpiminplylem2  33974  txomap  34025  qtophaus  34027  pcmplfinf  34052  zarcls1  34060  zarclsun  34061  zarclsint  34063  zarclssn  34064  zarcmplem  34072  rhmpreimacn  34076  pstmxmet  34088  pnfneige0  34142  esumcst  34254  esum2d  34284  esumiun  34285  ddemeas  34427  signsply0  34742  signstres  34766  prodfzo03  34794  actfunsnf1o  34795  actfunsnrndisj  34796  tgoldbachgt  34854  poimirlem17  38011  poimirlem20  38014  itg2gt0cn  38049  fdc1  38120  lhprelat3N  40539  dihjat2  41930  aks4d1p8  42579  primrootspoweq0  42598  aks6d1c4  42616  aks6d1c6isolem1  42666  aks6d1c6isolem2  42667  aks6d1c6lem5  42669  aks6d1c7  42676  rhmqusspan  42677  grpods  42686  unitscyglem1  42687  unitscyglem2  42688  unitscyglem3  42689  unitscyglem4  42690  aks5lem7  42692  aks5  42696  prjspersym  43064  eldioph2b  43219  diophrex  43231  irrapxlem6  43279  pellex  43287  pellfundex  43338  lnrfg  43571  mpaaeu  43602  cvgdvgrat  44764  climsuse  46060  limsupre  46091  limcleqr  46094  limsuppnfdlem  46151  liminflelimsuplem  46225  limsupub2  46262  xlimclim2lem  46289  climxlim2  46296  cncficcgt0  46338  dvbdfbdioo  46380  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  stoweidlem28  46478  stoweidlem29  46479  stoweidlem52  46502  stoweidlem60  46510  fourierdlem39  46596  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem114  46670  hspmbllem2  47077  nnsum4primesevenALTV  48299  imaf1co  49652