ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  reximi GIF version

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
StepHypRef Expression
1 reximi.1 . . 3 (𝜑𝜓)
21a1i 9 . 2 (𝑥𝐴 → (𝜑𝜓))
32reximia 2499 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator