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

Theorem 2albii 1686
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 1685 . 2  |-  ( A. y ph  <->  A. y ps )
32albii 1685 1  |-  ( A. x A. y ph  <->  A. x A. y ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187   A.wal 1435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676
This theorem depends on definitions:  df-bi 188
This theorem is referenced by:  sbcom2  2251  2sb6rf  2258  mo4f  2322  2mo2  2356  2mos  2358  r3al  2745  ralcomf  2926  nfnid  4593  raliunxp  4936  cnvsym  5176  intasym  5177  intirr  5180  codir  5182  qfto  5183  dffun4  5556  fun11  5609  fununi  5610  mpt22eqb  6363  aceq0  8500  zfac  8841  zfcndac  8995  addsrmo  9448  mulsrmo  9449  cotr2g  12984  isirred2  17872  2spotdisj  25731  rmo4fOLD  28074  bnj580  29676  bnj978  29712  axacprim  30286  dfso2  30345  dfpo2  30346  dfon2lem8  30387  dffun10  30630  wl-sbcom2d  31798  mpt2bi123f  32313  dford4  35797  isdomn3  35994  undmrnresiss  36123  cnvssco  36125  pm14.12  36685
  Copyright terms: Public domain W3C validator