Theorem reximia 3073

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  reximi  3076  iunpw  7726  tz7.49c  8387  fisup2g  9384  fiinf2g  9417  unwdomg  9501  trcl  9649  cfsmolem  10192  1idpr  10952  qmulz  12876  xrsupexmnf  13232  xrinfmexpnf  13233  caubnd2  15293  caurcvg  15612  caurcvg2  15613  caucvg  15614  sgrpidmnd  18676  txlm  23604  znegscl  28400  z12negscl  28486  norm1exi  31337  chrelat2i  32452  xrofsup  32857  esumcvg  34263  bnj168  34906  satfv1  35576  satfv0fvfmla0  35626  poimirlem30  37895  ismblfin  37906  dffltz  42986  allbutfi  45745  sge0ltfirpmpt  46760  ovolval5lem3  47006  2reu8i  47467  nnsum4primes4  48143  nnsum4primesprm  48145  nnsum4primesgbe  48147  nnsum4primesle9  48149  0aryfvalelfv  48989