Theorem r19.29an 3059

Description: A commonly used pattern based on r19.29 3054. (Contributed by Thierry Arnoux, 29-Dec-2019.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

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

Proof of Theorem r19.29an

Step	Hyp	Ref	Expression
1		nfv 1830	. . 3 ⊢ Ⅎ𝑥𝜑
2		nfre1 2988	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜓
3	1, 2	nfan 1816	. 2 ⊢ Ⅎ𝑥(𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)
4		r19.29an.1	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
5	4	adantllr 751	. 2 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
6		simpr 476	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 𝜓)
7	3, 5, 6	r19.29af 3058	1 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-ral 2901  df-rex 2902

This theorem is referenced by:  summolem2  14294  cygabl  18115  dissnlocfin  21142  utopsnneiplem  21861  restmetu  22185  elqaa  23881  colline  25344  f1otrg  25551  axcontlem2  25645  grpoidinvlem4  26745  2sqmo  28980  isarchi3  29072  fimaproj  29228  qtophaus  29231  locfinreflem  29235  cmpcref  29245  ordtconlem1  29298  esumpcvgval  29467  esumcvg  29475  eulerpartlems  29749  eulerpartlemgvv  29765  isbnd3  32753  eldiophss  36356  eldioph4b  36393  pellfund14b  36481  opeoALTV  40133