Theorem r19.29af 3274

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

Syntax hints:   → wi 4   ∧ wa 400  Ⅎwnf 1813   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-ral 3080  df-rex 3090

This theorem is referenced by:  fsnex  7281  neiptopnei  23289  neitr  23337  utopsnneiplem  24404  isucn2  24435  2sqmo  27601  foresf1o  32850  fsumiunle  33173  nsgqusf1olem3  33724  irngnzply1  34081  reff  34229  locfinreflem  34230  ordtconnlem1  34314  esumrnmpt2  34458  esumgect  34480  esum2dlem  34482  esum2d  34483  esumiun  34484  sigapildsys  34552  oms0  34687  eulerpartlemgvv  34766  breprexplema  35017  stoweidlem27  46741  stoweidlem35  46749