MPE Home 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  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
2albidv  |-  ( ph  ->  ( A. x A. y ps  <->  A. x A. y ch ) )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)    ch( x, y)

Proof of Theorem 2albidv
StepHypRef Expression
1 2albidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21albidv 1689 . 2  |-  ( ph  ->  ( A. y ps  <->  A. y ch ) )
32albidv 1689 1  |-  ( ph  ->  ( A. x A. y ps  <->  A. x A. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.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