Theorem 2albii 1646

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

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

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

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  sbcom2  2191  2sb6rf  2198  mo4f  2334  2mo2  2369  2mos  2372  2eu4OLD  2378  2eu6OLD  2381  r3al  2834  ralcomf  3013  nfnid  4666  raliunxp  5131  cnvsym  5369  intasym  5370  intirr  5373  codir  5375  qfto  5376  dffun4  5582  fun11  5635  fununi  5636  mpt22eqb  6384  aceq0  8490  zfac  8831  zfcndac  8986  addsrmo  9439  mulsrmo  9440  cotr2g  12894  isirred2  17545  2spotdisj  25263  rmo4fOLD  27593  axacprim  29320  dfso2  29424  dfpo2  29425  dfon2lem8  29462  dffun10  29792  wl-sbcom2d  30251  mpt2bi123f  30811  dford4  31210  isdomn3  31405  pm14.12  31569  bnj580  34372  bnj978  34408