Theorem reximia 3100

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  reximi  3103  iunpw  7771  tz7.49c  8434  fisup2g  9430  fiinf2g  9463  unwdomg  9547  trcl  9698  cfsmolem  10255  1idpr  11015  qmulz  12976  xrsupexmnf  13332  xrinfmexpnf  13333  caubnd2  15411  caurcvg  15730  caurcvg2  15731  caucvg  15732  sgrpidmnd  18798  txlm  23786  znegscl  28563  z12negscl  28649  norm1exi  31580  chrelat2i  32695  xrofsup  33090  esumcvg  34454  bnj168  35097  satfv1  35833  satfv0fvfmla0  35883  poimirlem30  38279  ismblfin  38290  dffltz  43346  allbutfi  46088  sge0ltfirpmpt  47102  ovolval5lem3  47348  2reu8i  47827  nnsum4primes4  48531  nnsum4primesprm  48533  nnsum4primesgbe  48535  nnsum4primesle9  48537  0aryfvalelfv  49392