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

Theorem ralimi2 2847
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 1633 . 2
3 df-ral 2812 . 2
4 df-ral 2812 . 2
52, 3, 43imtr4i 266 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393  e.wcel 1818  A.wral 2807
This theorem is referenced by:  ralimia  2848  ralcom3  3023  tfi  6688  resixpfo  7527  omex  8081  kmlem1  8551  brdom5  8928  brdom4  8929  xrub  11532  pcmptcl  14410  itgeq2  22184  iblcnlem  22195  pntrsumbnd  23751  nmounbseqi  25692  nmounbseqiOLD  25693  sumdmdi  27339  dmdbr4ati  27340  dmdbr6ati  27342  bnj110  33916  fiinfi  37758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator