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

Theorem 2albidv 1681
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 1679 . 2  |-  ( ph  ->  ( A. y ps  <->  A. y ch ) )
32albidv 1679 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 1367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  2moOLDOLD  2362  2eu6OLD  2372  dff13  5976  qliftfun  7190  seqf1o  11852  brfi1uzind  12224  dchrelbas3  22582  isass  23808  isch2  24631  mbfresfi  28443  trer  28516  ismrc  29042  2sbc6g  29674  lpolsetN  35132  islpolN  35133
  Copyright terms: Public domain W3C validator