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

Theorem ralimiaa 2788
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 2787 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 1756   A.wral 2713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2718
This theorem is referenced by:  ralrnmpt  5850  tz7.48-2  6895  mptelixpg  7298  boxriin  7303  acnlem  8216  iundom2g  8702  konigthlem  8730  hashge2el2dif  12182  rlim2  12972  prdsbas3  14417  prdsdsval2  14420  ptbasfi  19152  ptunimpt  19166  voliun  21033  riesz4i  25465  dmdbr6ati  25825  lgamgulmlem6  27018
  Copyright terms: Public domain W3C validator