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  7228  neiptopnei  23116  neitr  23164  utopsnneiplem  24231  isucn2  24262  2sqmo  27419  foresf1o  32593  fsumiunle  32922  nsgqusf1olem3  33499  irngnzply1  33884  reff  34032  locfinreflem  34033  ordtconnlem1  34117  esumrnmpt2  34261  esumgect  34283  esum2dlem  34285  esum2d  34286  esumiun  34287  sigapildsys  34355  oms0  34490  eulerpartlemgvv  34569  breprexplema  34823  stoweidlem27  46478  stoweidlem35  46486