Theorem reximi 2591

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

Syntax hints:   → wi 4   ∈ wcel 2164  ∃wrex 2473

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-ral 2477  df-rex 2478

This theorem is referenced by:  r19.29d2r  2638  r19.35-1  2644  r19.40  2648  reu3  2950  ssiun  3954  iinss  3964  elunirn  5809  tfrcllemssrecs  6405  nnawordex  6582  iinerm  6661  erovlem  6681  xpf1o  6900  fidcenumlemim  7011  omniwomnimkv  7226  genprndl  7581  genprndu  7582  appdiv0nq  7624  ltexprlemm  7660  recexsrlem  7834  rereceu  7949  recexre  8597  aprcl  8665  rexanre  11364  climi2  11431  climi0  11432  climcaucn  11494  prodmodclem2  11720  prodmodc  11721  gcdsupex  12094  gcdsupcl  12095  bezoutlemeu  12144  dfgcd3  12147  isnsgrp  12989  rhmdvdsr  13671  eltg2b  14222  lmcvg  14385  cnptoprest  14407  lmtopcnp  14418  txbas  14426  metrest  14674  elply2  14881  2sqlem7  15208  bj-charfunbi  15303  bj-findis  15471