Theorem r19.29af 3248

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

Syntax hints:   → wi 4   ∧ wa 396  Ⅎwnf 1790   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-ral 3054  df-rex 3064

This theorem is referenced by:  fsnex  7227  neiptopnei  23115  neitr  23163  utopsnneiplem  24230  isucn2  24261  2sqmo  27418  foresf1o  32592  fsumiunle  32921  nsgqusf1olem3  33498  irngnzply1  33875  reff  34023  locfinreflem  34024  ordtconnlem1  34108  esumrnmpt2  34252  esumgect  34274  esum2dlem  34276  esum2d  34277  esumiun  34278  sigapildsys  34346  oms0  34481  eulerpartlemgvv  34560  breprexplema  34814  stoweidlem27  46470  stoweidlem35  46478