MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximia Structured version   Unicode version

Theorem reximia 2892
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.)
Hypothesis
Ref Expression
reximia.1  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
reximia  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )

Proof of Theorem reximia
StepHypRef Expression
1 rexim 2891 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  -> 
( E. x  e.  A  ph  ->  E. x  e.  A  ps )
)
2 reximia.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2mprg 2789 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1869   E.wrex 2777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1661  df-ral 2781  df-rex 2782
This theorem is referenced by:  reximi  2894  iunpw  6617  wfrdmcl  7050  tz7.49c  7169  fisup2g  7988  fiinf2g  8020  unwdomg  8103  trcl  8215  cfsmolem  8702  1idpr  9456  qmulz  11269  zq  11272  xrsupexmnf  11592  xrinfmexpnf  11593  caubnd2  13414  caurcvg  13735  caurcvgOLD  13736  caurcvg2  13737  caucvg  13738  txlm  20655  norm1exi  26895  chrelat2i  28010  xrofsup  28353  esumcvg  28909  bnj168  29540  poimirlem30  31928  ismblfin  31939  sge0ltfirpmpt  38082  nnsum4primes4  38640  nnsum4primesprm  38642  nnsum4primesgbe  38644  nnsum4primesle9  38646
  Copyright terms: Public domain W3C validator