Theorem 2albii 1612

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 1611	. 2 |- ( A. y ph <-> A. y ps )
3	2	albii 1611	1 |- ( A. x A. y ph <-> A. x A. y ps )

Syntax hints:   <-> wb 184   A.wal 1368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  sbcom2  2160  2sb6rf  2169  mo4f  2325  2mo2  2368  2mos  2372  2eu4OLD  2378  2eu6OLD  2381  ralcomf  2985  nfnid  4632  raliunxp  5090  cnvsym  5323  intasym  5324  intirr  5327  codir  5329  qfto  5330  dffun4  5541  fun11  5594  fununi  5595  mpt22eqb  6312  aceq0  8403  zfac  8744  zfcndac  8901  isirred2  16926  rmo4fOLD  26059  axacprim  27525  dfso2  27731  dfpo2  27732  dfon2lem8  27770  dffun10  28112  wl-sbcom2d  28558  mpt2bi123f  29146  dford4  29549  isdomn3  29743  pm14.12  29846  2spotdisj  30825  bnj580  32261  bnj978  32297