Theorem r19.29af 3254

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

Syntax hints:   → wi 4   ∧ wa 399  Ⅎwnf 1785   ∈ wcel 2111  ∃wrex 3071

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 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-ral 3075  df-rex 3076

This theorem is referenced by:  fsnex  7031  neiptopnei  21832  neitr  21880  utopsnneiplem  22948  isucn2  22980  2sqmo  26120  foresf1o  30372  fsumiunle  30667  nsgqusf1olem3  31121  reff  31310  locfinreflem  31311  ordtconnlem1  31395  esumrnmpt2  31555  esumgect  31577  esum2dlem  31579  esum2d  31580  esumiun  31581  sigapildsys  31649  oms0  31783  eulerpartlemgvv  31862  breprexplema  32129  stoweidlem27  43035  stoweidlem35  43043