Theorem reximia 3081

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

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

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 3071

This theorem is referenced by:  reximi  3084  iunpw  7791  wfrdmclOLD  8357  tz7.49c  8486  fisup2g  9508  fiinf2g  9540  unwdomg  9624  trcl  9768  cfsmolem  10310  1idpr  11069  qmulz  12993  xrsupexmnf  13347  xrinfmexpnf  13348  caubnd2  15396  caurcvg  15713  caurcvg2  15714  caucvg  15715  sgrpidmnd  18752  txlm  23656  znegscl  28378  norm1exi  31269  chrelat2i  32384  xrofsup  32771  esumcvg  34087  bnj168  34744  satfv1  35368  satfv0fvfmla0  35418  poimirlem30  37657  ismblfin  37668  dffltz  42644  allbutfi  45404  sge0ltfirpmpt  46423  ovolval5lem3  46669  2reu8i  47125  nnsum4primes4  47776  nnsum4primesprm  47778  nnsum4primesgbe  47780  nnsum4primesle9  47782  0aryfvalelfv  48556