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

Theorem ralimiaa 2796
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 432 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32ralimia 2795 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1842   A.wral 2754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652
This theorem depends on definitions:  df-bi 185  df-an 369  df-ral 2759
This theorem is referenced by:  ralrnmpt  6018  tz7.48-2  7144  mptelixpg  7544  boxriin  7549  acnlem  8461  iundom2g  8947  konigthlem  8975  hashge2el2dif  12570  rlim2  13468  prdsbas3  15095  prdsdsval2  15098  ptbasfi  20374  ptunimpt  20388  voliun  22256  lgamgulmlem6  23689  riesz4i  27395  dmdbr6ati  27755
  Copyright terms: Public domain W3C validator