Theorem reximi 2604

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

Syntax hints:   → wi 4   ∈ wcel 2177  ∃wrex 2486

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-ral 2490  df-rex 2491

This theorem is referenced by:  r19.29d2r  2651  r19.35-1  2657  r19.40  2661  reu3  2964  ssiun  3971  iinss  3981  elunirn  5842  tfrcllemssrecs  6445  nnawordex  6622  iinerm  6701  erovlem  6721  xpf1o  6948  fidcenumlemim  7061  omniwomnimkv  7276  genprndl  7641  genprndu  7642  appdiv0nq  7684  ltexprlemm  7720  recexsrlem  7894  rereceu  8009  recexre  8658  aprcl  8726  rexanre  11575  climi2  11643  climi0  11644  climcaucn  11706  prodmodclem2  11932  prodmodc  11933  gcdsupex  12322  gcdsupcl  12323  bezoutlemeu  12372  dfgcd3  12375  isnsgrp  13282  rhmdvdsr  13981  eltg2b  14570  lmcvg  14733  cnptoprest  14755  lmtopcnp  14766  txbas  14774  metrest  15022  elply2  15251  2sqlem7  15642  bj-charfunbi  15821  bj-findis  15989