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

Theorem reximia 2824
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 2823 . 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 2788 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   E.wrex 2719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-ral 2723  df-rex 2724
This theorem is referenced by:  reximi  2826  iunpw  6393  tz7.49c  6904  fisup2g  7719  unwdomg  7802  trcl  7951  cfsmolem  8442  1idpr  9201  qmulz  10959  zq  10962  xrsupexmnf  11270  xrinfmexpnf  11271  caubnd2  12848  caurcvg  13157  caurcvg2  13158  caucvg  13159  txlm  19224  norm1exi  24656  chrelat2i  25772  xrofsup  26058  esumcvg  26538  wfrlem9  27735  ismblfin  28435  bnj168  31724
  Copyright terms: Public domain W3C validator