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

Theorem ralimiaa 2782
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 425 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32ralimia 2781 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726   A.wral 2707
This theorem is referenced by:  ralrnmpt  5880  tz7.48-2  6701  mptelixpg  7101  boxriin  7106  acnlem  7931  iundom2g  8417  konigthlem  8445  rlim2  12292  prdsbas3  13705  prdsdsval2  13708  ptbasfi  17615  ptunimpt  17629  voliun  19450  riesz4i  23568  dmdbr6ati  23928  lgamgulmlem6  24820
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-an 362  df-ral 2712
  Copyright terms: Public domain W3C validator