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  4011  iinss  4021  elunirn  5909  tfrcllemssrecs  6520  nnawordex  6699  iinerm  6778  erovlem  6798  xpf1o  7032  fidcenumlemim  7153  omniwomnimkv  7368  genprndl  7743  genprndu  7744  appdiv0nq  7786  ltexprlemm  7822  recexsrlem  7996  rereceu  8111  recexre  8760  aprcl  8828  rexanre  11800  climi2  11868  climi0  11869  climcaucn  11931  prodmodclem2  12158  prodmodc  12159  gcdsupex  12548  gcdsupcl  12549  bezoutlemeu  12598  dfgcd3  12601  isnsgrp  13509  rhmdvdsr  14210  eltg2b  14804  lmcvg  14967  cnptoprest  14989  lmtopcnp  15000  txbas  15008  metrest  15256  elply2  15485  2sqlem7  15876  umgr2edg1  16086  umgr2edgneu  16089  bj-charfunbi  16464  bj-findis  16632