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

Theorem ralimdv2 2786
 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:   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem ralimdv2
StepHypRef Expression
1 ralimdv2.1 . . 3
21alimdv 1631 . 2
3 df-ral 2710 . 2
4 df-ral 2710 . 2
52, 3, 43imtr4g 262 1
 Colors of variables: wff set class Syntax hints:   wi 4  wal 1549   wcel 1725  wral 2705 This theorem is referenced by:  ssralv  3407  zorn2lem7  8382  pwfseqlem3  8535  sup2  9964  xrsupexmnf  10883  xrinfmexpnf  10884  xrsupsslem  10885  xrinfmsslem  10886  xrub  10890  r19.29uz  12154  rexuzre  12156  caurcvg  12470  caucvg  12472  isprm5  13112  mrissmrid  13866  elcls3  17147  iscnp4  17327  cncls2  17337  cnntr  17339  2ndcsep  17522  dyadmbllem  19491  xrlimcnp  20807  pntlem3  21303  sigaclfu2  24504  climrec  27705  mapdordlem2  32435 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626 This theorem depends on definitions:  df-bi 178  df-ral 2710
 Copyright terms: Public domain W3C validator