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

Theorem 2albidv 1637
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 1635 . 2  |-  ( ph  ->  ( A. y ps  <->  A. y ch ) )
32albidv 1635 1  |-  ( ph  ->  ( A. x A. y ps  <->  A. x A. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549
This theorem is referenced by:  2mo  2359  2eu6  2366  dff13  6004  qliftfun  6989  seqf1o  11364  brfi1uzind  11715  dchrelbas3  21022  isass  21904  isch2  22726  mbfresfi  26253  trer  26319  ismrc  26755  2sbc6g  27592  lpolsetN  32280  islpolN  32281
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator