Theorem r19.29af 3273

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

Syntax hints:   → wi 4   ∧ wa 387  Ⅎwnf 1746   ∈ wcel 2050  ∃wrex 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-12 2106

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-nf 1747  df-ral 3094  df-rex 3095

This theorem is referenced by:  r19.29anOLD  3274  r19.29aOLD  3275  fsnex  6864  neiptopnei  21444  neitr  21492  utopsnneiplem  22559  isucn2  22591  2sqmo  25715  foresf1o  30044  fsumiunle  30291  reff  30744  locfinreflem  30745  ordtconnlem1  30808  esumrnmpt2  30968  esumgect  30990  esum2dlem  30992  esum2d  30993  esumiun  30994  sigapildsys  31063  oms0  31197  eulerpartlemgvv  31276  breprexplema  31546  stoweidlem27  41741  stoweidlem35  41749