Theorem reximia 3101

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)

Hypothesis

Ref	Expression
ralimia.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

Ref	Expression
reximia	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reximia

Step	Hyp	Ref	Expression
1		ralimia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
2	1	imdistani 579	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	reximi2 3099	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ 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

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

This theorem is used by:  reximi  3104  iunpw  7809  tz7.49c  8484  fisup2g  9488  fiinf2g  9521  unwdomg  9605  trcl  9756  cfsmolem  10375  1idpr  11141  qmulz  13105  xrsupexmnf  13462  xrinfmexpnf  13463  caubnd2  15554  caurcvg  15873  caurcvg2  15874  caucvg  15875  txlm  23997  znegscl  28808  z12negscl  28894  norm1exi  31882  chrelat2i  32997  xrofsup  33429  esumcvg  34788  bnj168  35431  satfv1  36295  satfv0fvfmla0  36345  poimirlem30  38760  ismblfin  38771  dffltz  43863  allbutfi  46609  sge0ltfirpmpt  47623  ovolval5lem3  47869  2reu8i  48389  nnsum4primes4  49092  nnsum4primesprm  49094  nnsum4primesgbe  49096  nnsum4primesle9  49098  0aryfvalelfv  49952