Theorem r19.29af 3058

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

Syntax hints:   → wi 4   ∧ wa 383  Ⅎwnf 1699   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701  df-ral 2901  df-rex 2902

This theorem is referenced by:  r19.29an  3059  r19.29a  3060  elsnxpOLD  5595  fsnex  6438  neiptopnei  20746  neitr  20794  utopsnneiplem  21861  isucn2  21893  foresf1o  28727  2sqmo  28980  reff  29234  locfinreflem  29235  ordtconlem1  29298  esumrnmpt2  29457  esumgect  29479  esum2dlem  29481  esum2d  29482  esumiun  29483  sigapildsys  29552  oms0  29686  eulerpartlemgvv  29765  stoweidlem27  38920  stoweidlem35  38928