Theorem reximia 3064

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  reximi  3067  iunpw  7711  tz7.49c  8375  fisup2g  9378  fiinf2g  9411  unwdomg  9495  trcl  9643  cfsmolem  10183  1idpr  10942  qmulz  12870  xrsupexmnf  13225  xrinfmexpnf  13226  caubnd2  15283  caurcvg  15602  caurcvg2  15603  caucvg  15604  sgrpidmnd  18631  txlm  23551  znegscl  28303  zs12negscl  28373  norm1exi  31212  chrelat2i  32327  xrofsup  32723  esumcvg  34052  bnj168  34696  satfv1  35335  satfv0fvfmla0  35385  poimirlem30  37629  ismblfin  37640  dffltz  42607  allbutfi  45373  sge0ltfirpmpt  46390  ovolval5lem3  46636  2reu8i  47098  nnsum4primes4  47774  nnsum4primesprm  47776  nnsum4primesgbe  47778  nnsum4primesle9  47780  0aryfvalelfv  48621