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

Step	Hyp	Ref	Expression
1		albii.1	. . 3 |- ( ph <-> ps )
2	1	albii 1615	. 2 |- ( A. y ph <-> A. y ps )
3	2	albii 1615	1 |- ( A. x A. y ph <-> A. x A. y ps )

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