Theorem r19.29af 3271

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

Syntax hints:   → wi 4   ∧ wa 399  Ⅎwnf 1803   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-nf 1804  df-ral 3077  df-rex 3087

This theorem is referenced by:  fsnex  7267  neiptopnei  23192  neitr  23240  utopsnneiplem  24307  isucn2  24338  2sqmo  27501  foresf1o  32703  fsumiunle  33031  nsgqusf1olem3  33601  irngnzply1  33988  reff  34136  locfinreflem  34137  ordtconnlem1  34221  esumrnmpt2  34365  esumgect  34387  esum2dlem  34389  esum2d  34390  esumiun  34391  sigapildsys  34459  oms0  34594  eulerpartlemgvv  34673  breprexplema  34924  stoweidlem27  46601  stoweidlem35  46609