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

Theorem reximia 2803
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 2802 . 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 2767 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  reximi  2805  iunpw  4751  tz7.49c  6695  abianfp  6708  fisup2g  7463  unwdomg  7544  trcl  7656  cfsmolem  8142  1idpr  8898  qmulz  10569  zq  10572  xrsupexmnf  10875  xrinfmexpnf  10876  caubnd2  12153  caurcvg  12462  caurcvg2  12463  caucvg  12464  txlm  17672  norm1exi  22744  chrelat2i  23860  xrofsup  24118  esumcvg  24468  wfrlem9  25538  ismblfin  26237  bnj168  29034
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator