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

Theorem ralimi2 2628
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
Hypothesis
Ref Expression
ralimi2.1  |-  ( ( x  e.  A  ->  ph )  ->  ( x  e.  B  ->  ps ) )
Assertion
Ref Expression
ralimi2  |-  ( A. x  e.  A  ph  ->  A. x  e.  B  ps )

Proof of Theorem ralimi2
StepHypRef Expression
1 ralimi2.1 . . 3  |-  ( ( x  e.  A  ->  ph )  ->  ( x  e.  B  ->  ps ) )
21alimi 1549 . 2  |-  ( A. x ( x  e.  A  ->  ph )  ->  A. x ( x  e.  B  ->  ps )
)
3 df-ral 2561 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2561 . 2  |-  ( A. x  e.  B  ps  <->  A. x ( x  e.  B  ->  ps )
)
52, 3, 43imtr4i 257 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530    e. wcel 1696   A.wral 2556
This theorem is referenced by:  ralimia  2629  ralcom3  2718  tfi  4660  resixpfo  6870  omex  7360  kmlem1  7792  brdom5  8170  brdom4  8171  xrub  10646  pcmptcl  12955  itgeq2  19148  iblcnlem  19159  pntrsumbnd  20731  nmounbseqi  21371  nmounbseqiOLD  21372  sumdmdi  23016  dmdbr4ati  23017  dmdbr6ati  23019  domintrefb  25166  bnj110  29206
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ral 2561
  Copyright terms: Public domain W3C validator