Theorem reximia 3100

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

Syntax hints:   → wi 4   ∈ wcel 2145  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  reximi  3103  iunpw  7758  tz7.49c  8421  fisup2g  9417  fiinf2g  9450  unwdomg  9534  trcl  9685  cfsmolem  10242  1idpr  11002  qmulz  12966  xrsupexmnf  13322  xrinfmexpnf  13323  caubnd2  15399  caurcvg  15718  caurcvg2  15719  caucvg  15720  sgrpidmnd  18787  txlm  23766  znegscl  28543  z12negscl  28629  norm1exi  31511  chrelat2i  32626  xrofsup  33024  esumcvg  34393  bnj168  35036  satfv1  35726  satfv0fvfmla0  35776  poimirlem30  38161  ismblfin  38172  dffltz  43228  allbutfi  45966  sge0ltfirpmpt  46980  ovolval5lem3  47226  2reu8i  47705  nnsum4primes4  48409  nnsum4primesprm  48411  nnsum4primesgbe  48413  nnsum4primesle9  48415  0aryfvalelfv  49266