Theorem r19.29af 3076

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

Syntax hints:   → wi 4   ∧ wa 384  Ⅎwnf 1708   ∈ wcel 1990  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-ral 2917  df-rex 2918

This theorem is referenced by:  r19.29an  3077  r19.29a  3078  elsnxpOLD  5678  fsnex  6538  neiptopnei  20936  neitr  20984  utopsnneiplem  22051  isucn2  22083  foresf1o  29343  fsumiunle  29575  2sqmo  29649  reff  29906  locfinreflem  29907  ordtconnlem1  29970  esumrnmpt2  30130  esumgect  30152  esum2dlem  30154  esum2d  30155  esumiun  30156  sigapildsys  30225  oms0  30359  eulerpartlemgvv  30438  breprexplema  30708  stoweidlem27  40244  stoweidlem35  40252