Theorem reximia 3065

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3054

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 3055

This theorem is referenced by:  reximi  3068  iunpw  7750  tz7.49c  8417  fisup2g  9427  fiinf2g  9460  unwdomg  9544  trcl  9688  cfsmolem  10230  1idpr  10989  qmulz  12917  xrsupexmnf  13272  xrinfmexpnf  13273  caubnd2  15331  caurcvg  15650  caurcvg2  15651  caucvg  15652  sgrpidmnd  18673  txlm  23542  znegscl  28287  zs12negscl  28347  norm1exi  31186  chrelat2i  32301  xrofsup  32697  esumcvg  34083  bnj168  34727  satfv1  35357  satfv0fvfmla0  35407  poimirlem30  37651  ismblfin  37662  dffltz  42629  allbutfi  45396  sge0ltfirpmpt  46413  ovolval5lem3  46659  2reu8i  47118  nnsum4primes4  47794  nnsum4primesprm  47796  nnsum4primesgbe  47798  nnsum4primesle9  47800  0aryfvalelfv  48628