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

Theorem ralimi2 2780
 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 1569 . 2
3 df-ral 2712 . 2
4 df-ral 2712 . 2
52, 3, 43imtr4i 259 1
 Colors of variables: wff set class Syntax hints:   wi 4  wal 1550   wcel 1726  wral 2707 This theorem is referenced by:  ralimia  2781  ralcom3  2875  tfi  4836  resixpfo  7103  omex  7601  kmlem1  8035  brdom5  8412  brdom4  8413  xrub  10895  pcmptcl  13265  itgeq2  19672  iblcnlem  19683  pntrsumbnd  21265  nmounbseqi  22283  nmounbseqiOLD  22284  sumdmdi  23928  dmdbr4ati  23929  dmdbr6ati  23931  bnj110  29302 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567 This theorem depends on definitions:  df-bi 179  df-ral 2712
 Copyright terms: Public domain W3C validator