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

Theorem reximia 2923
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 2922 . 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 2820 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762   E.wrex 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-ral 2812  df-rex 2813
This theorem is referenced by:  reximi  2925  iunpw  6585  tz7.49c  7101  fisup2g  7915  unwdomg  7999  trcl  8148  cfsmolem  8639  1idpr  9396  qmulz  11174  zq  11177  xrsupexmnf  11485  xrinfmexpnf  11486  caubnd2  13139  caurcvg  13448  caurcvg2  13449  caucvg  13450  txlm  19877  norm1exi  25830  chrelat2i  26946  xrofsup  27236  esumcvg  27718  wfrlem9  28914  ismblfin  29619  bnj168  32740
  Copyright terms: Public domain W3C validator