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

Theorem ralimi2 2746
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 1565 . 2  |-  ( A. x ( x  e.  A  ->  ph )  ->  A. x ( x  e.  B  ->  ps )
)
3 df-ral 2679 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2679 . 2  |-  ( A. x  e.  B  ps  <->  A. x ( x  e.  B  ->  ps )
)
52, 3, 43imtr4i 258 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546    e. wcel 1721   A.wral 2674
This theorem is referenced by:  ralimia  2747  ralcom3  2841  tfi  4800  resixpfo  7067  omex  7562  kmlem1  7994  brdom5  8371  brdom4  8372  xrub  10854  pcmptcl  13223  itgeq2  19630  iblcnlem  19641  pntrsumbnd  21221  nmounbseqi  22239  nmounbseqiOLD  22240  sumdmdi  23884  dmdbr4ati  23885  dmdbr6ati  23887  bnj110  28947
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ral 2679
  Copyright terms: Public domain W3C validator