Theorem r19.29af 3214

Description: A commonly used pattern based on r19.29 3210. (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 1992	. 2 ⊢ Ⅎ𝑥𝜒
3		r19.29af.1	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
4		r19.29af.2	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
5	1, 2, 3, 4	r19.29af2 3213	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383  Ⅎwnf 1857   ∈ wcel 2139  ∃wrex 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1854  df-nf 1859  df-ral 3055  df-rex 3056

This theorem is referenced by:  r19.29an  3215  r19.29a  3216  elsnxpOLD  5839  fsnex  6701  neiptopnei  21138  neitr  21186  utopsnneiplem  22252  isucn2  22284  foresf1o  29650  fsumiunle  29884  2sqmo  29958  reff  30215  locfinreflem  30216  ordtconnlem1  30279  esumrnmpt2  30439  esumgect  30461  esum2dlem  30463  esum2d  30464  esumiun  30465  sigapildsys  30534  oms0  30668  eulerpartlemgvv  30747  breprexplema  31017  stoweidlem27  40747  stoweidlem35  40755