Theorem reximia 3068

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 568	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	reximi2 3066	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  reximi  3071  iunpw  7710  tz7.49c  8371  fisup2g  9360  fiinf2g  9393  unwdomg  9477  trcl  9625  cfsmolem  10168  1idpr  10927  qmulz  12851  xrsupexmnf  13206  xrinfmexpnf  13207  caubnd2  15267  caurcvg  15586  caurcvg2  15587  caucvg  15588  sgrpidmnd  18649  txlm  23564  znegscl  28317  zs12negscl  28389  norm1exi  31232  chrelat2i  32347  xrofsup  32754  esumcvg  34120  bnj168  34763  satfv1  35428  satfv0fvfmla0  35478  poimirlem30  37710  ismblfin  37721  dffltz  42752  allbutfi  45515  sge0ltfirpmpt  46530  ovolval5lem3  46776  2reu8i  47237  nnsum4primes4  47913  nnsum4primesprm  47915  nnsum4primesgbe  47917  nnsum4primesle9  47919  0aryfvalelfv  48760