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

Theorem ralimia 2795
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 2794 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   A.wral 2754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652
This theorem depends on definitions:  df-bi 185  df-ral 2759
This theorem is referenced by:  ralimiaa  2796  ralimi  2797  r19.12  2933  rr19.3v  3191  rr19.28v  3192  exfo  6027  ffvresb  6041  f1mpt  6150  weniso  6233  ixpf  7529  ixpiunwdom  8051  tz9.12lem3  8239  dfac2a  8542  kmlem12  8573  axdc2lem  8860  ac6num  8891  ac6c4  8893  brdom6disj  8942  konigthlem  8975  arch  10833  cshw1  12846  serf0  13652  symgextfo  16771  baspartn  19747  ptcnplem  20414  rngmgmbs4  25833  spanuni  26876  lnopunilem1  27342  finixpnum  31410  indexa  31506  heiborlem5  31593  mzpincl  35028  dfac11  35370  stgoldbwt  37830  2zrngnmlid2  38268
  Copyright terms: Public domain W3C validator