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

Theorem reximi 2433
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 2431 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  wrex 2324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-ial 1443
This theorem depends on definitions:  df-bi 114  df-ral 2328  df-rex 2329
This theorem is referenced by:  r19.29d2r  2472  r19.35-1  2477  r19.40  2481  reu3  2753  ssiun  3726  iinss  3735  elunirn  5432  nnawordex  6131  iinerm  6208  erovlem  6228  genprndl  6676  genprndu  6677  appdiv0nq  6719  ltexprlemm  6755  recexsrlem  6916  rereceu  7020  recexre  7642  climi2  10039  climi0  10040  climcaucn  10100  bj-findis  10470
  Copyright terms: Public domain W3C validator