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

Theorem ralimi2 2788
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 1604 . 2  |-  ( A. x ( x  e.  A  ->  ph )  ->  A. x ( x  e.  B  ->  ps )
)
3 df-ral 2720 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2720 . 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 1367    e. wcel 1756   A.wral 2715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-ral 2720
This theorem is referenced by:  ralimia  2789  ralcom3  2886  tfi  6464  resixpfo  7301  omex  7849  kmlem1  8319  brdom5  8696  brdom4  8697  xrub  11274  pcmptcl  13953  itgeq2  21255  iblcnlem  21266  pntrsumbnd  22815  nmounbseqi  24177  nmounbseqiOLD  24178  sumdmdi  25824  dmdbr4ati  25825  dmdbr6ati  25827  bnj110  31851
  Copyright terms: Public domain W3C validator