Theorem reximia 3099

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3089

This theorem is used by:  reximi  3102  iunpw  7774  tz7.49c  8439  fisup2g  9443  fiinf2g  9476  unwdomg  9560  trcl  9711  cfsmolem  10276  1idpr  11042  qmulz  13004  xrsupexmnf  13361  xrinfmexpnf  13362  caubnd2  15449  caurcvg  15768  caurcvg2  15769  caucvg  15770  sgrpidmnd  18847  txlm  23880  znegscl  28665  z12negscl  28751  norm1exi  31739  chrelat2i  32854  xrofsup  33246  esumcvg  34604  bnj168  35248  satfv1  35950  satfv0fvfmla0  36000  poimirlem30  38407  ismblfin  38418  dffltz  43488  allbutfi  46230  sge0ltfirpmpt  47244  ovolval5lem3  47490  2reu8i  48009  nnsum4primes4  48713  nnsum4primesprm  48715  nnsum4primesgbe  48717  nnsum4primesle9  48719  0aryfvalelfv  49573