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

Theorem ralimiaa 2630
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 2629 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 1696   A.wral 2556
This theorem is referenced by:  ralrnmpt  5685  tz7.48-2  6470  mptelixpg  6869  boxriin  6874  acnlem  7691  iundom2g  8178  konigthlem  8206  rlim2  11986  prdsbas3  13396  prdsdsval2  13399  ptbasfi  17292  ptunimpt  17306  voliun  18927  riesz4i  22659  dmdbr6ati  23019  srefwref  25170  fprodadd  25455  fprodneg  25481  fprodsub  25482  tartarmap  25991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2561
  Copyright terms: Public domain W3C validator