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

Theorem ralimia 2629
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
Hypothesis
Ref Expression
ralimia.1  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
ralimia  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )

Proof of Theorem ralimia
StepHypRef Expression
1 ralimia.1 . . 3  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
21a2i 12 . 2  |-  ( ( x  e.  A  ->  ph )  ->  ( x  e.  A  ->  ps ) )
32ralimi2 2628 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   A.wral 2556
This theorem is referenced by:  ralimiaa  2630  ralimi  2631  r19.12  2669  rr19.3v  2922  rr19.28v  2923  exfo  5694  ffvresb  5706  f1mpt  5801  weniso  5868  ixpf  6854  ixpiunwdom  7321  tz9.12lem3  7477  dfac2a  7772  kmlem12  7803  axdc2lem  8090  ac6num  8122  ac6c4  8124  brdom6disj  8173  konigthlem  8206  arch  9978  serf0  12169  baspartn  16708  ptcnplem  17331  rngmgmbs4  21100  spanuni  22139  lnopunilem1  22606  prl2  25272  indexa  26515  heiborlem5  26642  mzpincl  26915  dfac11  27263
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-ral 2561
  Copyright terms: Public domain W3C validator