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

Theorem reximi 2459
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 2457 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   E.wrex 2350
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-ial 1468
This theorem depends on definitions:  df-bi 115  df-ral 2354  df-rex 2355
This theorem is referenced by:  r19.29d2r  2500  r19.35-1  2505  r19.40  2509  reu3  2783  ssiun  3722  iinss  3731  elunirn  5431  tfrcllemssrecs  5995  nnawordex  6160  iinerm  6237  erovlem  6257  xpf1o  6375  genprndl  6762  genprndu  6763  appdiv0nq  6805  ltexprlemm  6841  recexsrlem  7002  rereceu  7106  recexre  7734  rexanre  10233  climi2  10254  climi0  10255  climcaucn  10315  gcdsupex  10482  gcdsupcl  10483  bezoutlemeu  10529  dfgcd3  10532  bj-findis  10917
  Copyright terms: Public domain W3C validator