Theorem reximi 2527

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

Syntax hints:   → wi 4   ∈ wcel 1480  ∃wrex 2415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-ral 2419  df-rex 2420

This theorem is referenced by:  r19.29d2r  2574  r19.35-1  2579  r19.40  2583  reu3  2869  ssiun  3850  iinss  3859  elunirn  5660  tfrcllemssrecs  6242  nnawordex  6417  iinerm  6494  erovlem  6514  xpf1o  6731  fidcenumlemim  6833  genprndl  7322  genprndu  7323  appdiv0nq  7365  ltexprlemm  7401  recexsrlem  7575  rereceu  7690  recexre  8333  aprcl  8401  rexanre  10985  climi2  11050  climi0  11051  climcaucn  11113  gcdsupex  11635  gcdsupcl  11636  bezoutlemeu  11684  dfgcd3  11687  eltg2b  12212  lmcvg  12375  cnptoprest  12397  lmtopcnp  12408  txbas  12416  metrest  12664  bj-findis  13166