Theorem reximia 3067

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  reximi  3070  iunpw  7704  tz7.49c  8365  fisup2g  9353  fiinf2g  9386  unwdomg  9470  trcl  9618  cfsmolem  10158  1idpr  10917  qmulz  12846  xrsupexmnf  13201  xrinfmexpnf  13202  caubnd2  15262  caurcvg  15581  caurcvg2  15582  caucvg  15583  sgrpidmnd  18644  txlm  23561  znegscl  28314  zs12negscl  28386  norm1exi  31225  chrelat2i  32340  xrofsup  32745  esumcvg  34094  bnj168  34737  satfv1  35395  satfv0fvfmla0  35445  poimirlem30  37689  ismblfin  37700  dffltz  42666  allbutfi  45430  sge0ltfirpmpt  46445  ovolval5lem3  46691  2reu8i  47143  nnsum4primes4  47819  nnsum4primesprm  47821  nnsum4primesgbe  47823  nnsum4primesle9  47825  0aryfvalelfv  48666