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

Theorem ralimia 2813
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 14 . 2  |-  ( ( x  e.  A  ->  ph )  ->  ( x  e.  A  ->  ps ) )
32ralimi2 2812 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   A.wral 2771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676
This theorem depends on definitions:  df-bi 188  df-ral 2776
This theorem is referenced by:  ralimiaa  2814  ralimi  2815  r19.12  2951  rr19.3v  3212  rr19.28v  3213  exfo  6055  ffvresb  6069  f1mpt  6177  weniso  6260  ixpf  7555  ixpiunwdom  8115  tz9.12lem3  8268  dfac2a  8567  kmlem12  8598  axdc2lem  8885  ac6num  8916  ac6c4  8918  brdom6disj  8967  konigthlem  9000  arch  10873  cshw1  12923  serf0  13746  symgextfo  17062  baspartn  19967  ptcnplem  20634  rngmgmbs4  26143  spanuni  27195  lnopunilem1  27661  phpreu  31893  finixpnum  31894  poimirlem26  31930  indexa  32024  heiborlem5  32111  mzpincl  35545  dfac11  35890  stgoldbwt  38747  2zrngnmlid2  39571
  Copyright terms: Public domain W3C validator