Theorem r19.29an 3142

Description: A commonly used pattern in the spirit of r19.29 3101. (Contributed by Thierry Arnoux, 29-Dec-2019.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)

Hypothesis

Ref	Expression
rexlimdva2.1	⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
r19.29an	⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒)

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.29an

Step	Hyp	Ref	Expression
1		rexlimdva2.1	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
2	1	rexlimdva2 3141	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
3	2	imp 406	1 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  fimaproj  8078  summolem2  15669  ghmqusnsglem1  19246  ghmquskerlem1  19249  cygabl  19857  dissnlocfin  23504  utopsnneiplem  24222  restmetu  24545  elqaa  26299  2sqmo  27414  colline  28731  axcontlem2  29048  grpoidinvlem4  30593  2ndimaxp  32734  fnpreimac  32758  mndlrinvb  33100  mndlactfo  33102  mndractfo  33104  mndlactf1o  33105  mndractf1o  33106  cyc3genpm  33228  isarchi3  33263  elrgspn  33322  elrgspnsubrun  33325  fracerl  33382  dvdsruasso  33460  dvdsruasso2  33461  grplsmid  33479  quslsm  33480  nsgqusf1olem2  33489  nsgqusf1olem3  33490  elrspunidl  33503  elrspunsn  33504  ssdifidllem  33531  ssdifidlprm  33533  ssmxidllem  33548  1arithidom  33612  1arithufdlem3  33621  fldextrspunlsp  33834  constrconj  33905  constrfin  33906  constrelextdg2  33907  constrfiss  33911  ist0cld  33993  qtophaus  33996  locfinreflem  34000  cmpcref  34010  ordtconnlem1  34084  esumpcvgval  34238  esumcvg  34246  eulerpartlems  34520  eulerpartlemgvv  34536  reprinfz1  34782  reprpmtf1o  34786  satffunlem2lem2  35604  isbnd3  38119  eldiophss  43220  eldioph4b  43257  pellfund14b  43345  opeoALTV  48172