Theorem reximia 3071

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3061

This theorem is referenced by:  reximi  3074  iunpw  7763  wfrdmclOLD  8329  tz7.49c  8458  fisup2g  9479  fiinf2g  9512  unwdomg  9596  trcl  9740  cfsmolem  10282  1idpr  11041  qmulz  12965  xrsupexmnf  13319  xrinfmexpnf  13320  caubnd2  15374  caurcvg  15691  caurcvg2  15692  caucvg  15693  sgrpidmnd  18715  txlm  23584  znegscl  28295  norm1exi  31177  chrelat2i  32292  xrofsup  32690  esumcvg  34063  bnj168  34707  satfv1  35331  satfv0fvfmla0  35381  poimirlem30  37620  ismblfin  37631  dffltz  42604  allbutfi  45368  sge0ltfirpmpt  46385  ovolval5lem3  46631  2reu8i  47090  nnsum4primes4  47751  nnsum4primesprm  47753  nnsum4primesgbe  47755  nnsum4primesle9  47757  0aryfvalelfv  48563