Theorem r19.29an 3143

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

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

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 3064

This theorem is referenced by:  fimaproj  8075  summolem2  15669  ghmqusnsglem1  19246  ghmquskerlem1  19249  cygabl  19857  dissnlocfin  23512  utopsnneiplem  24230  restmetu  24553  elqaa  26306  2sqmo  27418  colline  28735  axcontlem2  29052  grpoidinvlem4  30596  2ndimaxp  32738  fnpreimac  32762  mndlrinvb  33104  mndlactfo  33106  mndractfo  33108  mndlactf1o  33109  mndractf1o  33110  cyc3genpm  33233  isarchi3  33268  elrgspn  33327  elrgspnsubrun  33330  fracerl  33390  dvdsruasso  33468  dvdsruasso2  33469  grplsmid  33487  quslsm  33488  nsgqusf1olem2  33497  nsgqusf1olem3  33498  elrspunidl  33511  elrspunsn  33512  ssdifidllem  33539  ssdifidlprm  33541  ssmxidllem  33556  1arithidom  33620  1arithufdlem3  33629  fldextrspunlsp  33858  constrconj  33929  constrfin  33930  constrelextdg2  33931  constrfiss  33935  ist0cld  34017  qtophaus  34020  locfinreflem  34024  cmpcref  34034  ordtconnlem1  34108  esumpcvgval  34262  esumcvg  34270  eulerpartlems  34544  eulerpartlemgvv  34560  reprinfz1  34806  reprpmtf1o  34810  satffunlem2lem2  35634  isbnd3  38151  eldiophss  43223  eldioph4b  43256  pellfund14b  43344  opeoALTV  48175