Theorem reximddv3 3183

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022.)

Hypotheses

Ref	Expression
reximddv3.1	⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
reximddv3.2	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Assertion

Ref	Expression
reximddv3	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximddv3

Step	Hyp	Ref	Expression
1		reximddv3.1	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
2	1	anasss 472	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
3		reximddv3.2	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
4	2, 3	reximddv 3182	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  inagcgrasubbtwn  33083  inagcgrabtwn  33084  iscgrag  33085  cgrgptxfr  33086  leawittrg  33094  edompidlem  33940  rprmasso2  34142  rprmirredlem  34146  rnmptlb  46470  rnmptbddlem  46471  limclner  46876  climisp  46971  climrescn  46973  liminflbuz2  47040  liminflimsupxrre  47042  climxlim2lem  47070  hoicvr  47773