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

Theorem reximi 2529
 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 2527 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1480  ∃wrex 2417 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514 This theorem depends on definitions:  df-bi 116  df-ral 2421  df-rex 2422 This theorem is referenced by:  r19.29d2r  2576  r19.35-1  2581  r19.40  2585  reu3  2874  ssiun  3858  iinss  3867  elunirn  5670  tfrcllemssrecs  6252  nnawordex  6427  iinerm  6504  erovlem  6524  xpf1o  6741  fidcenumlemim  6843  omniwomnimkv  7044  genprndl  7348  genprndu  7349  appdiv0nq  7391  ltexprlemm  7427  recexsrlem  7601  rereceu  7716  recexre  8359  aprcl  8427  rexanre  11016  climi2  11081  climi0  11082  climcaucn  11144  prodmodclem2  11370  prodmodc  11371  gcdsupex  11669  gcdsupcl  11670  bezoutlemeu  11718  dfgcd3  11721  eltg2b  12249  lmcvg  12412  cnptoprest  12434  lmtopcnp  12445  txbas  12453  metrest  12701  bj-findis  13321
 Copyright terms: Public domain W3C validator