Theorem r19.29af 3246

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

Syntax hints:   → wi 4   ∧ wa 395  Ⅎwnf 1783   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3045  df-rex 3054

This theorem is referenced by:  fsnex  7258  neiptopnei  23019  neitr  23067  utopsnneiplem  24135  isucn2  24166  2sqmo  27348  foresf1o  32433  fsumiunle  32754  nsgqusf1olem3  33386  irngnzply1  33686  reff  33829  locfinreflem  33830  ordtconnlem1  33914  esumrnmpt2  34058  esumgect  34080  esum2dlem  34082  esum2d  34083  esumiun  34084  sigapildsys  34152  oms0  34288  eulerpartlemgvv  34367  breprexplema  34621  stoweidlem27  46025  stoweidlem35  46033