Theorem reximia 3078

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∃wrex 3067

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  reximi  3081  iunpw  7789  wfrdmclOLD  8355  tz7.49c  8484  fisup2g  9505  fiinf2g  9537  unwdomg  9621  trcl  9765  cfsmolem  10307  1idpr  11066  qmulz  12990  xrsupexmnf  13343  xrinfmexpnf  13344  caubnd2  15392  caurcvg  15709  caurcvg2  15710  caucvg  15711  sgrpidmnd  18764  txlm  23671  znegscl  28392  norm1exi  31278  chrelat2i  32393  xrofsup  32777  esumcvg  34066  bnj168  34722  satfv1  35347  satfv0fvfmla0  35397  poimirlem30  37636  ismblfin  37647  dffltz  42620  allbutfi  45342  sge0ltfirpmpt  46363  ovolval5lem3  46609  2reu8i  47062  nnsum4primes4  47713  nnsum4primesprm  47715  nnsum4primesgbe  47717  nnsum4primesle9  47719  0aryfvalelfv  48484