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

Theorem reximia 2819
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 2818 . 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 2783 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   E.wrex 2714
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 2718  df-rex 2719
This theorem is referenced by:  reximi  2821  iunpw  6389  tz7.49c  6897  fisup2g  7712  unwdomg  7795  trcl  7944  cfsmolem  8435  1idpr  9194  qmulz  10952  zq  10955  xrsupexmnf  11263  xrinfmexpnf  11264  caubnd2  12841  caurcvg  13150  caurcvg2  13151  caucvg  13152  txlm  19180  norm1exi  24588  chrelat2i  25704  xrofsup  25988  esumcvg  26471  wfrlem9  27661  ismblfin  28357  bnj168  31555
  Copyright terms: Public domain W3C validator