Theorem reximia 3080

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

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

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

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

This theorem is referenced by:  reximi  3083  iunpw  7675  wfrdmclOLD  8210  tz7.49c  8339  fisup2g  9317  fiinf2g  9349  unwdomg  9433  trcl  9577  cfsmolem  10119  1idpr  10878  qmulz  12784  xrsupexmnf  13132  xrinfmexpnf  13133  caubnd2  15160  caurcvg  15479  caurcvg2  15480  caucvg  15481  sgrpidmnd  18479  txlm  22897  norm1exi  29841  chrelat2i  30956  xrofsup  31318  esumcvg  32293  bnj168  32950  satfv1  33565  satfv0fvfmla0  33615  poimirlem30  35905  ismblfin  35916  dffltz  40721  allbutfi  43257  sge0ltfirpmpt  44272  ovolval5lem3  44518  2reu8i  44945  nnsum4primes4  45581  nnsum4primesprm  45583  nnsum4primesgbe  45585  nnsum4primesle9  45587  0aryfvalelfv  46321