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

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  reximi  3084  iunpw  7760  wfrdmclOLD  8319  tz7.49c  8448  fisup2g  9465  fiinf2g  9497  unwdomg  9581  trcl  9725  cfsmolem  10267  1idpr  11026  qmulz  12939  xrsupexmnf  13288  xrinfmexpnf  13289  caubnd2  15308  caurcvg  15627  caurcvg2  15628  caucvg  15629  sgrpidmnd  18664  txlm  23372  norm1exi  30758  chrelat2i  31873  xrofsup  32235  esumcvg  33370  bnj168  34027  satfv1  34640  satfv0fvfmla0  34690  poimirlem30  36821  ismblfin  36832  dffltz  41678  allbutfi  44402  sge0ltfirpmpt  45423  ovolval5lem3  45669  2reu8i  46120  nnsum4primes4  46756  nnsum4primesprm  46758  nnsum4primesgbe  46760  nnsum4primesle9  46762  0aryfvalelfv  47409