Theorem reximi 2629

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

Syntax hints:   → wi 4   ∈ wcel 2202  ∃wrex 2511

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 2515  df-rex 2516

This theorem is referenced by:  rexanaliim  2638  r19.29d2r  2677  r19.35-1  2683  r19.40  2687  reu3  2996  ssiun  4012  iinss  4022  elunirn  5907  tfrcllemssrecs  6518  nnawordex  6697  iinerm  6776  erovlem  6796  xpf1o  7030  fidcenumlemim  7151  omniwomnimkv  7366  genprndl  7741  genprndu  7742  appdiv0nq  7784  ltexprlemm  7820  recexsrlem  7994  rereceu  8109  recexre  8758  aprcl  8826  rexanre  11782  climi2  11850  climi0  11851  climcaucn  11913  prodmodclem2  12140  prodmodc  12141  gcdsupex  12530  gcdsupcl  12531  bezoutlemeu  12580  dfgcd3  12583  isnsgrp  13491  rhmdvdsr  14192  eltg2b  14781  lmcvg  14944  cnptoprest  14966  lmtopcnp  14977  txbas  14985  metrest  15233  elply2  15462  2sqlem7  15853  umgr2edg1  16063  umgr2edgneu  16066  bj-charfunbi  16427  bj-findis  16595