Theorem reximia 3103

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃wrex 3092

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3093

This theorem is used by:  reximi  3106  iunpw  7779  tz7.49c  8442  fisup2g  9439  fiinf2g  9472  unwdomg  9556  trcl  9707  cfsmolem  10272  1idpr  11032  qmulz  12993  xrsupexmnf  13349  xrinfmexpnf  13350  caubnd2  15435  caurcvg  15754  caurcvg2  15755  caucvg  15756  sgrpidmnd  18826  txlm  23842  znegscl  28622  z12negscl  28708  norm1exi  31639  chrelat2i  32754  xrofsup  33149  esumcvg  34507  bnj168  35151  satfv1  35876  satfv0fvfmla0  35926  poimirlem30  38342  ismblfin  38353  dffltz  43407  allbutfi  46149  sge0ltfirpmpt  47163  ovolval5lem3  47409  2reu8i  47891  nnsum4primes4  48595  nnsum4primesprm  48597  nnsum4primesgbe  48599  nnsum4primesle9  48601  0aryfvalelfv  49456