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

Theorem 2albii 1616
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 1615 . 2  |-  ( A. y ph  <->  A. y ps )
32albii 1615 1  |-  ( A. x A. y ph  <->  A. x A. y ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  sbcom2  2158  2sb6rf  2167  mo4f  2321  2mos  2365  2eu4  2369  2eu6  2371  ralcomf  2877  nfnid  4518  raliunxp  4975  cnvsym  5209  intasym  5210  intirr  5213  codir  5215  qfto  5216  dffun4  5427  fun11  5480  fununi  5481  mpt22eqb  6198  aceq0  8284  zfac  8625  zfcndac  8782  isirred2  16783  rmo4fOLD  25799  axacprim  27271  dfso2  27477  dfpo2  27478  dfon2lem8  27516  dffun10  27858  wl-sbcom2d  28300  mpt2bi123f  28884  dford4  29287  isdomn3  29481  pm14.12  29584  2spotdisj  30563  bnj580  31723  bnj978  31759
  Copyright terms: Public domain W3C validator