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

Theorem reximia 2920
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 2919 . 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 2817 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-ral 2809  df-rex 2810
This theorem is referenced by:  reximi  2922  iunpw  6587  tz7.49c  7103  fisup2g  7918  unwdomg  8002  trcl  8150  cfsmolem  8641  1idpr  9396  qmulz  11186  zq  11189  xrsupexmnf  11499  xrinfmexpnf  11500  caubnd2  13272  caurcvg  13581  caurcvg2  13582  caucvg  13583  txlm  20315  norm1exi  26366  chrelat2i  27482  xrofsup  27816  esumcvg  28315  wfrlem9  29591  ismblfin  30295  bnj168  34186
  Copyright terms: Public domain W3C validator