Theorem r19.29af 3057

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

Syntax hints:   → wi 4   ∧ wa 382  Ⅎwnf 1698   ∈ wcel 1976  ∃wrex 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ex 1695  df-nf 1700  df-ral 2900  df-rex 2901

This theorem is referenced by:  r19.29an  3058  r19.29a  3059  elsnxpOLD  5581  fsnex  6416  neiptopnei  20694  neitr  20742  utopsnneiplem  21809  isucn2  21841  foresf1o  28561  2sqmo  28814  reff  29068  locfinreflem  29069  ordtconlem1  29132  esumrnmpt2  29291  esumgect  29313  esum2dlem  29315  esum2d  29316  esumiun  29317  sigapildsys  29386  oms0  29520  eulerpartlemgvv  29599  stoweidlem27  38744  stoweidlem35  38752