Theorem r19.29af 3105

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

Syntax hints:   → wi 4   ∧ wa 383  Ⅎwnf 1748   ∈ wcel 2030  ∃wrex 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-ral 2946  df-rex 2947

This theorem is referenced by:  r19.29an  3106  r19.29a  3107  elsnxpOLD  5716  fsnex  6578  neiptopnei  20984  neitr  21032  utopsnneiplem  22098  isucn2  22130  foresf1o  29469  fsumiunle  29703  2sqmo  29777  reff  30034  locfinreflem  30035  ordtconnlem1  30098  esumrnmpt2  30258  esumgect  30280  esum2dlem  30282  esum2d  30283  esumiun  30284  sigapildsys  30353  oms0  30487  eulerpartlemgvv  30566  breprexplema  30836  stoweidlem27  40562  stoweidlem35  40570