Theorem reximia 3075

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  reximi  3078  iunpw  7721  tz7.49c  8382  fisup2g  9379  fiinf2g  9412  unwdomg  9496  trcl  9647  cfsmolem  10190  1idpr  10950  qmulz  12899  xrsupexmnf  13255  xrinfmexpnf  13256  caubnd2  15318  caurcvg  15637  caurcvg2  15638  caucvg  15639  sgrpidmnd  18705  txlm  23638  znegscl  28409  z12negscl  28495  norm1exi  31346  chrelat2i  32461  xrofsup  32866  esumcvg  34277  bnj168  34920  satfv1  35598  satfv0fvfmla0  35648  poimirlem30  38024  ismblfin  38035  dffltz  43091  allbutfi  45844  sge0ltfirpmpt  46858  ovolval5lem3  47104  2reu8i  47583  nnsum4primes4  48287  nnsum4primesprm  48289  nnsum4primesgbe  48291  nnsum4primesle9  48293  0aryfvalelfv  49133