Theorem reximi 2628

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

Syntax hints:   → wi 4   ∈ wcel 2201  ∃wrex 2510

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-ral 2514  df-rex 2515

This theorem is referenced by:  rexanaliim  2637  r19.29d2r  2676  r19.35-1  2682  r19.40  2686  reu3  2995  ssiun  4013  iinss  4023  elunirn  5912  tfrcllemssrecs  6523  nnawordex  6702  iinerm  6781  erovlem  6801  xpf1o  7035  fidcenumlemim  7156  omniwomnimkv  7371  genprndl  7746  genprndu  7747  appdiv0nq  7789  ltexprlemm  7825  recexsrlem  7999  rereceu  8114  recexre  8763  aprcl  8831  rexanre  11803  climi2  11871  climi0  11872  climcaucn  11934  prodmodclem2  12161  prodmodc  12162  gcdsupex  12551  gcdsupcl  12552  bezoutlemeu  12601  dfgcd3  12604  isnsgrp  13512  rhmdvdsr  14213  eltg2b  14807  lmcvg  14970  cnptoprest  14992  lmtopcnp  15003  txbas  15011  metrest  15259  elply2  15488  2sqlem7  15879  umgr2edg1  16089  umgr2edgneu  16092  bj-charfunbi  16466  bj-findis  16634