Theorem r19.29af 3333

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

Syntax hints:   → wi 4   ∧ wa 398  Ⅎwnf 1784   ∈ wcel 2114  ∃wrex 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-ral 3145  df-rex 3146

This theorem is referenced by:  r19.29anOLD  3334  r19.29aOLD  3335  fsnex  7041  neiptopnei  21742  neitr  21790  utopsnneiplem  22858  isucn2  22890  2sqmo  26015  foresf1o  30267  fsumiunle  30547  reff  31105  locfinreflem  31106  ordtconnlem1  31169  esumrnmpt2  31329  esumgect  31351  esum2dlem  31353  esum2d  31354  esumiun  31355  sigapildsys  31423  oms0  31557  eulerpartlemgvv  31636  breprexplema  31903  stoweidlem27  42319  stoweidlem35  42327