Theorem r19.29af 3330

Description: A commonly used pattern based on r19.29 3253. See r19.29a 3288, r19.29an 3287 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 3329	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398  Ⅎwnf 1783   ∈ wcel 2113  ∃wrex 3138

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 1969  ax-7 2014  ax-12 2176

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-nf 1784  df-ral 3142  df-rex 3143

This theorem is referenced by:  r19.29anOLD  3331  r19.29aOLD  3332  fsnex  7032  neiptopnei  21735  neitr  21783  utopsnneiplem  22851  isucn2  22883  2sqmo  26011  foresf1o  30264  fsumiunle  30545  reff  31127  locfinreflem  31128  ordtconnlem1  31188  esumrnmpt2  31348  esumgect  31370  esum2dlem  31372  esum2d  31373  esumiun  31374  sigapildsys  31442  oms0  31576  eulerpartlemgvv  31655  breprexplema  31922  stoweidlem27  42386  stoweidlem35  42394