Theorem reximia 3097

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  reximi  3100  iunpw  7785  tz7.49c  8459  fisup2g  9464  fiinf2g  9497  unwdomg  9581  trcl  9732  cfsmolem  10351  1idpr  11117  qmulz  13081  xrsupexmnf  13438  xrinfmexpnf  13439  caubnd2  15530  caurcvg  15849  caurcvg2  15850  caucvg  15851  sgrpidmnd  18933  txlm  23972  znegscl  28783  z12negscl  28869  norm1exi  31857  chrelat2i  32972  xrofsup  33405  esumcvg  34764  bnj168  35407  satfv1  36214  satfv0fvfmla0  36264  poimirlem30  38661  ismblfin  38672  dffltz  43763  allbutfi  46497  sge0ltfirpmpt  47511  ovolval5lem3  47757  2reu8i  48276  nnsum4primes4  48980  nnsum4primesprm  48982  nnsum4primesgbe  48984  nnsum4primesle9  48986  0aryfvalelfv  49840