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

Theorem ralimiaa 2617
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
ralimiaa.1  |-  ( ( x  e.  A  /\  ph )  ->  ps )
Assertion
Ref Expression
ralimiaa  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )

Proof of Theorem ralimiaa
StepHypRef Expression
1 ralimiaa.1 . . 3  |-  ( ( x  e.  A  /\  ph )  ->  ps )
21ex 423 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32ralimia 2616 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralrnmpt  5669  tz7.48-2  6454  mptelixpg  6853  boxriin  6858  acnlem  7675  iundom2g  8162  konigthlem  8190  rlim2  11970  prdsbas3  13380  prdsdsval2  13383  ptbasfi  17276  ptunimpt  17290  voliun  18911  riesz4i  22643  dmdbr6ati  23003  srefwref  24479  fprodadd  24764  fprodneg  24790  fprodsub  24791  tartarmap  25300
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2548
  Copyright terms: Public domain W3C validator