Theorem reximia 3087

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

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  reximi  3090  iunpw  7806  wfrdmclOLD  8373  tz7.49c  8502  fisup2g  9537  fiinf2g  9569  unwdomg  9653  trcl  9797  cfsmolem  10339  1idpr  11098  qmulz  13016  xrsupexmnf  13367  xrinfmexpnf  13368  caubnd2  15406  caurcvg  15725  caurcvg2  15726  caucvg  15727  sgrpidmnd  18777  txlm  23677  znegscl  28396  norm1exi  31282  chrelat2i  32397  xrofsup  32774  esumcvg  34050  bnj168  34706  satfv1  35331  satfv0fvfmla0  35381  poimirlem30  37610  ismblfin  37621  dffltz  42589  allbutfi  45308  sge0ltfirpmpt  46329  ovolval5lem3  46575  2reu8i  47028  nnsum4primes4  47663  nnsum4primesprm  47665  nnsum4primesgbe  47667  nnsum4primesle9  47669  0aryfvalelfv  48369