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

Theorem reximi 2470
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)
Hypothesis
Ref Expression
reximi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
reximi  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )

Proof of Theorem reximi
StepHypRef Expression
1 reximi.1 . . 3  |-  ( ph  ->  ps )
21a1i 9 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32reximia 2468 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1438   E.wrex 2360
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-ral 2364  df-rex 2365
This theorem is referenced by:  r19.29d2r  2512  r19.35-1  2517  r19.40  2521  reu3  2805  ssiun  3772  iinss  3781  elunirn  5545  tfrcllemssrecs  6117  nnawordex  6287  iinerm  6364  erovlem  6384  xpf1o  6560  fidcenumlemim  6661  genprndl  7080  genprndu  7081  appdiv0nq  7123  ltexprlemm  7159  recexsrlem  7320  rereceu  7424  recexre  8055  rexanre  10653  climi2  10676  climi0  10677  climcaucn  10740  gcdsupex  11227  gcdsupcl  11228  bezoutlemeu  11274  dfgcd3  11277  bj-findis  11874
  Copyright terms: Public domain W3C validator