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

Theorem ralimiaa 2849
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 434 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32ralimia 2848 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1762   A.wral 2807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812
This theorem is referenced by:  ralrnmpt  6021  tz7.48-2  7097  mptelixpg  7496  boxriin  7501  acnlem  8418  iundom2g  8904  konigthlem  8932  hashge2el2dif  12474  rlim2  13268  prdsbas3  14725  prdsdsval2  14728  ptbasfi  19810  ptunimpt  19824  voliun  21692  riesz4i  26644  dmdbr6ati  27004  lgamgulmlem6  28202
  Copyright terms: Public domain W3C validator