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

Theorem 2albidv 1617
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 1615 . 2  |-  ( ph  ->  ( A. y ps  <->  A. y ch ) )
32albidv 1615 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 1530
This theorem is referenced by:  2mo  2234  2eu6  2241  dff13  5799  qliftfun  6759  seqf1o  11103  dchrelbas3  20493  isass  20999  isch2  21819  elfuns  24525  trer  26330  ismrc  26879  2sbc6g  27718  lpolsetN  32294  islpolN  32295
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator