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

Theorem reximi 2504
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 2502 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1463   E.wrex 2392
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497
This theorem depends on definitions:  df-bi 116  df-ral 2396  df-rex 2397
This theorem is referenced by:  r19.29d2r  2551  r19.35-1  2556  r19.40  2560  reu3  2845  ssiun  3823  iinss  3832  elunirn  5633  tfrcllemssrecs  6215  nnawordex  6390  iinerm  6467  erovlem  6487  xpf1o  6704  fidcenumlemim  6806  genprndl  7293  genprndu  7294  appdiv0nq  7336  ltexprlemm  7372  recexsrlem  7546  rereceu  7661  recexre  8303  aprcl  8370  rexanre  10932  climi2  10997  climi0  10998  climcaucn  11060  gcdsupex  11542  gcdsupcl  11543  bezoutlemeu  11591  dfgcd3  11594  eltg2b  12118  lmcvg  12281  cnptoprest  12303  lmtopcnp  12314  txbas  12322  metrest  12570  bj-findis  12979
  Copyright terms: Public domain W3C validator