Theorem r19.29af 3271

Description: A commonly used pattern based on r19.29 3125. See r19.29a 3170, r19.29an 3166 for a variant when 𝑥 is disjoint from 𝜑. (Contributed by Thierry Arnoux, 29-Nov-2017.)

Hypotheses

Ref	Expression
r19.29af.0	⊢ Ⅎ𝑥𝜑
r19.29af.1	⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
r19.29af.2	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Assertion

Ref	Expression
r19.29af	⊢ (𝜑 → 𝜒)

Distinct variable group:   𝜒,𝑥

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

Proof of Theorem r19.29af

Step	Hyp	Ref	Expression
1		r19.29af.0	. 2 ⊢ Ⅎ𝑥𝜑
2		nfv 1946	. 2 ⊢ Ⅎ𝑥𝜒
3		r19.29af.1	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
4		r19.29af.2	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
5	1, 2, 3, 4	r19.29af2 3270	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  Ⅎwnf 1815   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-ral 3077  df-rex 3087

This theorem is used by:  fsnex  7295  neiptopnei  23459  neitr  23507  utopsnneiplem  24575  isucn2  24606  2sqmo  27773  foresf1o  33151  fsumiunle  33470  nsgqusf1olem3  34016  irngnzply1  34373  reff  34521  locfinreflem  34522  ordtconnlem1  34606  esumrnmpt2  34750  esumgect  34772  esum2dlem  34774  esum2d  34775  esumiun  34776  sigapildsys  34845  oms0  34979  eulerpartlemgvv  35058  breprexplema  35309  stoweidlem27  47173  stoweidlem35  47181