Theorem reximi 2594

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)

Hypothesis

Ref	Expression
reximi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
reximi	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reximi

Step	Hyp	Ref	Expression
1		reximi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 9	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	reximia 2592	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2167  ∃wrex 2476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-ral 2480  df-rex 2481

This theorem is referenced by:  r19.29d2r  2641  r19.35-1  2647  r19.40  2651  reu3  2954  ssiun  3959  iinss  3969  elunirn  5816  tfrcllemssrecs  6419  nnawordex  6596  iinerm  6675  erovlem  6695  xpf1o  6914  fidcenumlemim  7027  omniwomnimkv  7242  genprndl  7605  genprndu  7606  appdiv0nq  7648  ltexprlemm  7684  recexsrlem  7858  rereceu  7973  recexre  8622  aprcl  8690  rexanre  11402  climi2  11470  climi0  11471  climcaucn  11533  prodmodclem2  11759  prodmodc  11760  gcdsupex  12149  gcdsupcl  12150  bezoutlemeu  12199  dfgcd3  12202  isnsgrp  13108  rhmdvdsr  13807  eltg2b  14374  lmcvg  14537  cnptoprest  14559  lmtopcnp  14570  txbas  14578  metrest  14826  elply2  15055  2sqlem7  15446  bj-charfunbi  15541  bj-findis  15709