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  3958  iinss  3968  elunirn  5813  tfrcllemssrecs  6410  nnawordex  6587  iinerm  6666  erovlem  6686  xpf1o  6905  fidcenumlemim  7018  omniwomnimkv  7233  genprndl  7588  genprndu  7589  appdiv0nq  7631  ltexprlemm  7667  recexsrlem  7841  rereceu  7956  recexre  8605  aprcl  8673  rexanre  11385  climi2  11453  climi0  11454  climcaucn  11516  prodmodclem2  11742  prodmodc  11743  gcdsupex  12124  gcdsupcl  12125  bezoutlemeu  12174  dfgcd3  12177  isnsgrp  13049  rhmdvdsr  13731  eltg2b  14290  lmcvg  14453  cnptoprest  14475  lmtopcnp  14486  txbas  14494  metrest  14742  elply2  14971  2sqlem7  15362  bj-charfunbi  15457  bj-findis  15625