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

Theorem ralimi2 2615
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 1546 . 2  |-  ( A. x ( x  e.  A  ->  ph )  ->  A. x ( x  e.  B  ->  ps )
)
3 df-ral 2548 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2548 . 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 1527    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralimia  2616  ralcom3  2705  tfi  4644  resixpfo  6854  omex  7344  kmlem1  7776  brdom5  8154  brdom4  8155  xrub  10630  pcmptcl  12939  itgeq2  19132  iblcnlem  19143  pntrsumbnd  20715  nmounbseqi  21355  nmounbseqiOLD  21356  sumdmdi  23000  dmdbr4ati  23001  dmdbr6ati  23003  domintrefb  25063  bnj110  28890
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