Theorem reximia 3073

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  reximi  3076  iunpw  7718  tz7.49c  8378  fisup2g  9375  fiinf2g  9408  unwdomg  9492  trcl  9640  cfsmolem  10183  1idpr  10943  qmulz  12892  xrsupexmnf  13248  xrinfmexpnf  13249  caubnd2  15311  caurcvg  15630  caurcvg2  15631  caucvg  15632  sgrpidmnd  18698  txlm  23623  znegscl  28398  z12negscl  28484  norm1exi  31336  chrelat2i  32451  xrofsup  32855  esumcvg  34246  bnj168  34889  satfv1  35561  satfv0fvfmla0  35611  poimirlem30  37985  ismblfin  37996  dffltz  43081  allbutfi  45840  sge0ltfirpmpt  46854  ovolval5lem3  47100  2reu8i  47573  nnsum4primes4  48277  nnsum4primesprm  48279  nnsum4primesgbe  48281  nnsum4primesle9  48283  0aryfvalelfv  49123