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

Theorem ralimia 2771
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 2770 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   A.wral 2697
This theorem is referenced by:  ralimiaa  2772  ralimi  2773  r19.12  2811  rr19.3v  3069  rr19.28v  3070  exfo  5879  ffvresb  5892  f1mpt  5999  weniso  6067  ixpf  7076  ixpiunwdom  7551  tz9.12lem3  7707  dfac2a  8002  kmlem12  8033  axdc2lem  8320  ac6num  8351  ac6c4  8353  brdom6disj  8402  konigthlem  8435  arch  10210  serf0  12466  baspartn  17011  ptcnplem  17645  rngmgmbs4  21997  spanuni  23038  lnopunilem1  23505  indexa  26426  heiborlem5  26515  mzpincl  26782  dfac11  27128  cshw1  28238
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-ral 2702
  Copyright terms: Public domain W3C validator