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

Theorem ralimia 2817
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 13 . 2  |-  ( ( x  e.  A  ->  ph )  ->  ( x  e.  A  ->  ps ) )
32ralimi2 2816 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   A.wral 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-ral 2804
This theorem is referenced by:  ralimiaa  2818  ralimi  2819  r19.12  2936  rr19.3v  3208  rr19.28v  3209  exfo  5971  ffvresb  5984  f1mpt  6084  weniso  6155  ixpf  7396  ixpiunwdom  7918  tz9.12lem3  8108  dfac2a  8411  kmlem12  8442  axdc2lem  8729  ac6num  8760  ac6c4  8762  brdom6disj  8811  konigthlem  8844  arch  10688  cshw1  12575  serf0  13277  symgextfo  16047  baspartn  18692  ptcnplem  19327  rngmgmbs4  24057  spanuni  25100  lnopunilem1  25567  finixpnum  28563  indexa  28776  heiborlem5  28863  mzpincl  29219  dfac11  29564
  Copyright terms: Public domain W3C validator