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

Theorem reximia 2771
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 2770 . 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 2735 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   E.wrex 2667
This theorem is referenced by:  reximi  2773  iunpw  4718  tz7.49c  6662  abianfp  6675  fisup2g  7427  unwdomg  7508  trcl  7620  cfsmolem  8106  1idpr  8862  qmulz  10533  zq  10536  xrsupexmnf  10839  xrinfmexpnf  10840  caubnd2  12116  caurcvg  12425  caurcvg2  12426  caucvg  12427  txlm  17633  norm1exi  22705  chrelat2i  23821  xrofsup  24079  esumcvg  24429  wfrlem9  25478  ismblfin  26146  bnj168  28803
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 2671  df-rex 2672
  Copyright terms: Public domain W3C validator