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

Theorem ralimi2 2780
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 1569 . 2  |-  ( A. x ( x  e.  A  ->  ph )  ->  A. x ( x  e.  B  ->  ps )
)
3 df-ral 2712 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2712 . 2  |-  ( A. x  e.  B  ps  <->  A. x ( x  e.  B  ->  ps )
)
52, 3, 43imtr4i 259 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550    e. wcel 1726   A.wral 2707
This theorem is referenced by:  ralimia  2781  ralcom3  2875  tfi  4836  resixpfo  7103  omex  7601  kmlem1  8035  brdom5  8412  brdom4  8413  xrub  10895  pcmptcl  13265  itgeq2  19672  iblcnlem  19683  pntrsumbnd  21265  nmounbseqi  22283  nmounbseqiOLD  22284  sumdmdi  23928  dmdbr4ati  23929  dmdbr6ati  23931  bnj110  29302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-ral 2712
  Copyright terms: Public domain W3C validator