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 2113  ∃wrex 3060

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 3061

This theorem is referenced by:  reximi  3074  iunpw  7716  tz7.49c  8377  fisup2g  9372  fiinf2g  9405  unwdomg  9489  trcl  9637  cfsmolem  10180  1idpr  10940  qmulz  12864  xrsupexmnf  13220  xrinfmexpnf  13221  caubnd2  15281  caurcvg  15600  caurcvg2  15601  caucvg  15602  sgrpidmnd  18664  txlm  23592  znegscl  28388  z12negscl  28474  norm1exi  31325  chrelat2i  32440  xrofsup  32847  esumcvg  34243  bnj168  34886  satfv1  35557  satfv0fvfmla0  35607  poimirlem30  37847  ismblfin  37858  dffltz  42873  allbutfi  45633  sge0ltfirpmpt  46648  ovolval5lem3  46894  2reu8i  47355  nnsum4primes4  48031  nnsum4primesprm  48033  nnsum4primesgbe  48035  nnsum4primesle9  48037  0aryfvalelfv  48877