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

Theorem reximia 2754
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 2753 . 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 2718 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   E.wrex 2650
This theorem is referenced by:  reximi  2756  iunpw  4699  tz7.49c  6639  abianfp  6652  fisup2g  7404  unwdomg  7485  trcl  7597  cfsmolem  8083  1idpr  8839  qmulz  10509  zq  10512  xrsupexmnf  10815  xrinfmexpnf  10816  caubnd2  12088  caurcvg  12397  caurcvg2  12398  caucvg  12399  txlm  17601  norm1exi  22600  chrelat2i  23716  xrofsup  23962  esumcvg  24272  wfrlem9  25288  bnj168  28435
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-ral 2654  df-rex 2655
  Copyright terms: Public domain W3C validator