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

Theorem ralimia 2616
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 2615 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralimiaa  2617  ralimi  2618  r19.12  2656  rr19.3v  2909  rr19.28v  2910  exfo  5678  ffvresb  5690  f1mpt  5785  weniso  5852  ixpf  6838  ixpiunwdom  7305  tz9.12lem3  7461  dfac2a  7756  kmlem12  7787  axdc2lem  8074  ac6num  8106  ac6c4  8108  brdom6disj  8157  konigthlem  8190  arch  9962  serf0  12153  baspartn  16692  ptcnplem  17315  rngmgmbs4  21084  spanuni  22123  lnopunilem1  22590  prl2  25169  indexa  26412  heiborlem5  26539  mzpincl  26812  dfac11  27160
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ral 2548
  Copyright terms: Public domain W3C validator