Theorem r19.29af 3275

Description: A commonly used pattern based on r19.29 3129. See r19.29a 3174, r19.29an 3170 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 1949	. 2 ⊢ Ⅎ𝑥𝜒
3		r19.29af.1	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
4		r19.29af.2	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
5	1, 2, 3, 4	r19.29af2 3274	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  Ⅎwnf 1816   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3081  df-rex 3091

This theorem is used by:  fsnex  7322  neiptopnei  23505  neitr  23553  utopsnneiplem  24621  isucn2  24652  2sqmo  27821  foresf1o  33199  fsumiunle  33516  nsgqusf1olem3  34070  irngnzply1  34434  reff  34582  locfinreflem  34583  ordtconnlem1  34667  esumrnmpt2  34811  esumgect  34833  esum2dlem  34835  esum2d  34836  esumiun  34837  sigapildsys  34906  oms0  35040  eulerpartlemgvv  35119  breprexplema  35370  stoweidlem27  47310  stoweidlem35  47318