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

Theorem 2albidv 1613
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 1611 . 2  |-  ( ph  ->  ( A. y ps  <->  A. y ch ) )
32albidv 1611 1  |-  ( ph  ->  ( A. x A. y ps  <->  A. x A. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527
This theorem is referenced by:  2mo  2221  2eu6  2228  dff13  5783  qliftfun  6743  seqf1o  11087  dchrelbas3  20477  isass  20983  isch2  21803  elfuns  24454  trer  26227  ismrc  26776  2sbc6g  27615  lpolsetN  31672  islpolN  31673
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator