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

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

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