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

Theorem 2albii 1577
Description: Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.)
Hypothesis
Ref Expression
albii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
2albii  |-  ( A. x A. y ph  <->  A. x A. y ps )

Proof of Theorem 2albii
StepHypRef Expression
1 albii.1 . . 3  |-  ( ph  <->  ps )
21albii 1576 . 2  |-  ( A. y ph  <->  A. y ps )
32albii 1576 1  |-  ( A. x A. y ph  <->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1550
This theorem is referenced by:  sbcom  2166  mo4f  2315  2mos  2362  2eu4  2366  2eu6  2368  ralcomf  2868  nfnid  4395  raliunxp  5016  cnvsym  5250  intasym  5251  intirr  5254  codir  5256  qfto  5257  dffun4  5468  fun11  5518  fununi  5519  mpt22eqb  6181  aceq0  8001  zfac  8342  zfcndac  8496  isirred2  15808  rmo4fOLD  23985  axacprim  25158  dfso2  25379  dfpo2  25380  dfon2lem8  25419  dffun10  25761  dford4  27102  isdomn3  27502  pm14.12  27600  2spotdisj  28512  bnj580  29346  bnj978  29382  ax7w15AUX7  29730  ax7w14AUX7  29732  ax7w13AUX7  29735  ax7w17lem2AUX7  29738
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator