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 1947	. 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 1816   ∈ wcel 2145  ∃wrex 3086

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 1943  ax-6 2000  ax-7 2041  ax-12 2213

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

This theorem is used by:  fsnex  7285  neiptopnei  23358  neitr  23406  utopsnneiplem  24474  isucn2  24505  2sqmo  27674  foresf1o  32980  fsumiunle  33300  nsgqusf1olem3  33845  irngnzply1  34202  reff  34350  locfinreflem  34351  ordtconnlem1  34435  esumrnmpt2  34579  esumgect  34601  esum2dlem  34603  esum2d  34604  esumiun  34605  sigapildsys  34674  oms0  34809  eulerpartlemgvv  34888  breprexplema  35139  stoweidlem27  46856  stoweidlem35  46864