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

Theorem ralimia 2855
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 2854 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ral 2819
This theorem is referenced by:  ralimiaa  2856  ralimi  2857  r19.12  2988  rr19.3v  3245  rr19.28v  3246  exfo  6037  ffvresb  6050  f1mpt  6155  weniso  6236  ixpf  7488  ixpiunwdom  8013  tz9.12lem3  8203  dfac2a  8506  kmlem12  8537  axdc2lem  8824  ac6num  8855  ac6c4  8857  brdom6disj  8906  konigthlem  8939  arch  10788  cshw1  12747  serf0  13459  symgextfo  16239  baspartn  19219  ptcnplem  19854  rngmgmbs4  25092  spanuni  26135  lnopunilem1  26602  finixpnum  29612  indexa  29825  heiborlem5  29912  mzpincl  30268  dfac11  30612
  Copyright terms: Public domain W3C validator