Theorem reximia 3070

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

Syntax hints:   → wi 4   ∈ wcel 2098  ∃wrex 3059

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3060

This theorem is referenced by:  reximi  3073  iunpw  7774  wfrdmclOLD  8338  tz7.49c  8467  fisup2g  9493  fiinf2g  9525  unwdomg  9609  trcl  9753  cfsmolem  10295  1idpr  11054  qmulz  12968  xrsupexmnf  13319  xrinfmexpnf  13320  caubnd2  15340  caurcvg  15659  caurcvg2  15660  caucvg  15661  sgrpidmnd  18702  txlm  23596  znegscl  28289  norm1exi  31132  chrelat2i  32247  xrofsup  32619  esumcvg  33836  bnj168  34492  satfv1  35104  satfv0fvfmla0  35154  poimirlem30  37254  ismblfin  37265  dffltz  42193  allbutfi  44913  sge0ltfirpmpt  45934  ovolval5lem3  46180  2reu8i  46631  nnsum4primes4  47266  nnsum4primesprm  47268  nnsum4primesgbe  47270  nnsum4primesle9  47272  0aryfvalelfv  47894