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

Theorem 2albidv 1691
 Description: Formula-building rule for 2 universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
2albidv.1
Assertion
Ref Expression
2albidv
Distinct variable groups:   ,   ,
Allowed substitution hints:   (,)   (,)

Proof of Theorem 2albidv
StepHypRef Expression
1 2albidv.1 . . 3
21albidv 1689 . 2
32albidv 1689 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184  wal 1377 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680 This theorem depends on definitions:  df-bi 185 This theorem is referenced by:  2moOLDOLD  2384  2eu6OLD  2394  dff13  6165  qliftfun  7408  seqf1o  12128  brfi1uzind  12512  dchrelbas3  23377  isass  25149  isch2  25972  mclsssvlem  28754  mclsval  28755  mclsax  28761  mclsind  28762  mbfresfi  29995  trer  30068  ismrc  30567  2sbc6g  31230  lpolsetN  36685  islpolN  36686
 Copyright terms: Public domain W3C validator