Theorem reximi 2501

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

Syntax hints:   → wi 4   ∈ wcel 1461  ∃wrex 2389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-ial 1495

This theorem depends on definitions:  df-bi 116  df-ral 2393  df-rex 2394

This theorem is referenced by:  r19.29d2r  2548  r19.35-1  2553  r19.40  2557  reu3  2841  ssiun  3819  iinss  3828  elunirn  5619  tfrcllemssrecs  6200  nnawordex  6375  iinerm  6452  erovlem  6472  xpf1o  6688  fidcenumlemim  6789  genprndl  7270  genprndu  7271  appdiv0nq  7313  ltexprlemm  7349  recexsrlem  7510  rereceu  7617  recexre  8251  rexanre  10877  climi2  10942  climi0  10943  climcaucn  11005  gcdsupex  11487  gcdsupcl  11488  bezoutlemeu  11534  dfgcd3  11537  eltg2b  12059  lmcvg  12221  cnptoprest  12243  lmtopcnp  12254  txbas  12262  metrest  12488  bj-findis  12856