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
Assertion
Ref Expression
ralimi2

Proof of Theorem ralimi2
StepHypRef Expression
1 ralimi2.1 . . 3
21alimi 1680 . 2
3 df-ral 2778 . 2
4 df-ral 2778 . 2
52, 3, 43imtr4i 269 1
 Colors of variables: wff setvar class Syntax hints:   wi 4  wal 1435   wcel 1867  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