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

Theorem reximi 2567
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 2565 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2141  wrex 2449
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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527
This theorem depends on definitions:  df-bi 116  df-ral 2453  df-rex 2454
This theorem is referenced by:  r19.29d2r  2614  r19.35-1  2620  r19.40  2624  reu3  2920  ssiun  3913  iinss  3922  elunirn  5742  tfrcllemssrecs  6328  nnawordex  6504  iinerm  6581  erovlem  6601  xpf1o  6818  fidcenumlemim  6925  omniwomnimkv  7139  genprndl  7470  genprndu  7471  appdiv0nq  7513  ltexprlemm  7549  recexsrlem  7723  rereceu  7838  recexre  8484  aprcl  8552  rexanre  11171  climi2  11238  climi0  11239  climcaucn  11301  prodmodclem2  11527  prodmodc  11528  gcdsupex  11899  gcdsupcl  11900  bezoutlemeu  11949  dfgcd3  11952  isnsgrp  12634  eltg2b  12807  lmcvg  12970  cnptoprest  12992  lmtopcnp  13003  txbas  13011  metrest  13259  2sqlem7  13710  bj-charfunbi  13806  bj-findis  13974
  Copyright terms: Public domain W3C validator