Theorem reximia 3096

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∃wrex 3085

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  reximi  3099  iunpw  7750  tz7.49c  8412  fisup2g  9412  fiinf2g  9445  unwdomg  9529  trcl  9680  cfsmolem  10224  1idpr  10984  qmulz  12949  xrsupexmnf  13305  xrinfmexpnf  13306  caubnd2  15368  caurcvg  15687  caurcvg2  15688  caucvg  15689  sgrpidmnd  18756  txlm  23688  znegscl  28462  z12negscl  28548  norm1exi  31399  chrelat2i  32514  xrofsup  32919  esumcvg  34344  bnj168  34990  satfv1  35677  satfv0fvfmla0  35727  poimirlem30  38113  ismblfin  38124  dffltz  43180  allbutfi  45932  sge0ltfirpmpt  46946  ovolval5lem3  47192  2reu8i  47671  nnsum4primes4  48375  nnsum4primesprm  48377  nnsum4primesgbe  48379  nnsum4primesle9  48381  0aryfvalelfv  49221