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

Theorem ralimi2 2813
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 1680 . 2  |-  ( A. x ( x  e.  A  ->  ph )  ->  A. x ( x  e.  B  ->  ps )
)
3 df-ral 2778 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
4 df-ral 2778 . 2  |-  ( A. x  e.  B  ps  <->  A. x ( x  e.  B  ->  ps )
)
52, 3, 43imtr4i 269 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1435    e. wcel 1867   A.wral 2773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-ral 2778
This theorem is referenced by:  ralimia  2814  ralcom3  2992  tfi  6685  resixpfo  7559  omex  8139  kmlem1  8569  brdom5  8946  brdom4  8947  xrub  11586  pcmptcl  14788  itgeq2  22609  iblcnlem  22620  pntrsumbnd  24264  nmounbseqi  26260  nmounbseqiALT  26261  sumdmdi  27905  dmdbr4ati  27906  dmdbr6ati  27908  bnj110  29454  fiinfi  35880
  Copyright terms: Public domain W3C validator