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

Theorem reximia 2813
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 2812 . 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 2777 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   E.wrex 2708
This theorem is referenced by:  reximi  2815  iunpw  4762  tz7.49c  6706  abianfp  6719  fisup2g  7474  unwdomg  7555  trcl  7667  cfsmolem  8155  1idpr  8911  qmulz  10582  zq  10585  xrsupexmnf  10888  xrinfmexpnf  10889  caubnd2  12166  caurcvg  12475  caurcvg2  12476  caucvg  12477  txlm  17685  norm1exi  22757  chrelat2i  23873  xrofsup  24131  esumcvg  24481  wfrlem9  25551  ismblfin  26259  bnj168  29171
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-ral 2712  df-rex 2713
  Copyright terms: Public domain W3C validator