Theorem r19.29af 3259

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

Syntax hints:   → wi 4   ∧ wa 395  Ⅎwnf 1787   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-ral 3068  df-rex 3069

This theorem is referenced by:  fsnex  7135  neiptopnei  22191  neitr  22239  utopsnneiplem  23307  isucn2  23339  2sqmo  26490  foresf1o  30751  fsumiunle  31045  nsgqusf1olem3  31502  reff  31691  locfinreflem  31692  ordtconnlem1  31776  esumrnmpt2  31936  esumgect  31958  esum2dlem  31960  esum2d  31961  esumiun  31962  sigapildsys  32030  oms0  32164  eulerpartlemgvv  32243  breprexplema  32510  stoweidlem27  43458  stoweidlem35  43466