Theorem reximia 3098

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 3096	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3087

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 3088

This theorem is used by:  reximi  3101  iunpw  7774  tz7.49c  8440  fisup2g  9445  fiinf2g  9478  unwdomg  9562  trcl  9713  cfsmolem  10329  1idpr  11095  qmulz  13059  xrsupexmnf  13416  xrinfmexpnf  13417  caubnd2  15505  caurcvg  15824  caurcvg2  15825  caucvg  15826  sgrpidmnd  18908  txlm  23947  znegscl  28760  z12negscl  28846  norm1exi  31834  chrelat2i  32949  xrofsup  33341  esumcvg  34700  bnj168  35344  satfv1  36097  satfv0fvfmla0  36147  poimirlem30  38536  ismblfin  38547  dffltz  43624  allbutfi  46348  sge0ltfirpmpt  47362  ovolval5lem3  47608  2reu8i  48127  nnsum4primes4  48831  nnsum4primesprm  48833  nnsum4primesgbe  48835  nnsum4primesle9  48837  0aryfvalelfv  49691