Theorem r19.29af 3263

Description: A commonly used pattern based on r19.29 3112. See r19.29a 3160, r19.29an 3156 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 3262	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394  Ⅎwnf 1783   ∈ wcel 2104  ∃wrex 3068

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 1911  ax-6 1969  ax-7 2009  ax-12 2169

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-nf 1784  df-ral 3060  df-rex 3069

This theorem is referenced by:  fsnex  7283  neiptopnei  22856  neitr  22904  utopsnneiplem  23972  isucn2  24004  2sqmo  27176  foresf1o  32009  fsumiunle  32302  nsgqusf1olem3  32800  irngnzply1  33044  reff  33117  locfinreflem  33118  ordtconnlem1  33202  esumrnmpt2  33364  esumgect  33386  esum2dlem  33388  esum2d  33389  esumiun  33390  sigapildsys  33458  oms0  33594  eulerpartlemgvv  33673  breprexplema  33940  stoweidlem27  45041  stoweidlem35  45049