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

Theorem ralimdv2 2864
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
Hypothesis
Ref Expression
ralimdv2.1
Assertion
Ref Expression
ralimdv2
Distinct variable group:   ,

Proof of Theorem ralimdv2
StepHypRef Expression
1 ralimdv2.1 . . 3
21alimdv 1709 . 2
3 df-ral 2812 . 2
4 df-ral 2812 . 2
52, 3, 43imtr4g 270 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:  ralimdva  2865  ssralv  3563  zorn2lem7  8903  pwfseqlem3  9059  sup2  10524  xrsupexmnf  11525  xrinfmexpnf  11526  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  r19.29uz  13183  rexuzre  13185  caurcvg  13499  caucvg  13501  isprm5  14253  mrissmrid  15038  elcls3  19584  iscnp4  19764  cncls2  19774  cnntr  19776  2ndcsep  19960  dyadmbllem  22008  xrlimcnp  23298  pntlem3  23794  sigaclfu2  28121  climrec  31609  0ellimcdiv  31655  mapdordlem2  37364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator