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

Theorem ralimi2 2847
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 1634 . 2  |-  ( A. x ( x  e.  A  ->  ph )  ->  A. x ( x  e.  B  ->  ps )
)
3 df-ral 2812 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2812 . 2  |-  ( A. x  e.  B  ps  <->  A. x ( x  e.  B  ->  ps )
)
52, 3, 43imtr4i 266 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1393    e. wcel 1819   A.wral 2807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632
This theorem depends on definitions:  df-bi 185  df-ral 2812
This theorem is referenced by:  ralimia  2848  ralcom3  3023  tfi  6687  resixpfo  7526  omex  8077  kmlem1  8547  brdom5  8924  brdom4  8925  xrub  11528  pcmptcl  14421  itgeq2  22309  iblcnlem  22320  pntrsumbnd  23876  nmounbseqi  25818  nmounbseqiALT  25819  sumdmdi  27465  dmdbr4ati  27466  dmdbr6ati  27468  bnj110  34017  fiinfi  37859
  Copyright terms: Public domain W3C validator