Theorem reximia 3071

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3060

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 3061

This theorem is referenced by:  reximi  3074  iunpw  7765  wfrdmclOLD  8331  tz7.49c  8460  fisup2g  9481  fiinf2g  9514  unwdomg  9598  trcl  9742  cfsmolem  10284  1idpr  11043  qmulz  12967  xrsupexmnf  13321  xrinfmexpnf  13322  caubnd2  15376  caurcvg  15693  caurcvg2  15694  caucvg  15695  sgrpidmnd  18717  txlm  23586  znegscl  28332  zs12negscl  28392  norm1exi  31231  chrelat2i  32346  xrofsup  32744  esumcvg  34117  bnj168  34761  satfv1  35385  satfv0fvfmla0  35435  poimirlem30  37674  ismblfin  37685  dffltz  42657  allbutfi  45420  sge0ltfirpmpt  46437  ovolval5lem3  46683  2reu8i  47142  nnsum4primes4  47803  nnsum4primesprm  47805  nnsum4primesgbe  47807  nnsum4primesle9  47809  0aryfvalelfv  48615