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

Theorem reximi 2574
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 2572 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2148   E.wrex 2456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534
This theorem depends on definitions:  df-bi 117  df-ral 2460  df-rex 2461
This theorem is referenced by:  r19.29d2r  2621  r19.35-1  2627  r19.40  2631  reu3  2928  ssiun  3929  iinss  3939  elunirn  5767  tfrcllemssrecs  6353  nnawordex  6530  iinerm  6607  erovlem  6627  xpf1o  6844  fidcenumlemim  6951  omniwomnimkv  7165  genprndl  7520  genprndu  7521  appdiv0nq  7563  ltexprlemm  7599  recexsrlem  7773  rereceu  7888  recexre  8535  aprcl  8603  rexanre  11229  climi2  11296  climi0  11297  climcaucn  11359  prodmodclem2  11585  prodmodc  11586  gcdsupex  11958  gcdsupcl  11959  bezoutlemeu  12008  dfgcd3  12011  isnsgrp  12812  eltg2b  13557  lmcvg  13720  cnptoprest  13742  lmtopcnp  13753  txbas  13761  metrest  14009  2sqlem7  14471  bj-charfunbi  14566  bj-findis  14734
  Copyright terms: Public domain W3C validator