Theorem 2albii 1748

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

Syntax hints:   <-> wb 196   A.wal 1481

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

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  sbcom2  2445  2sb6rf  2452  mo4f  2516  2mo2  2550  2mos  2552  r3al  2940  ralcomf  3096  nfnid  4897  raliunxp  5261  cnvsym  5510  intasym  5511  intirr  5514  codir  5516  qfto  5517  dffun4  5900  fun11  5963  fununi  5964  mpt22eqb  6769  aceq0  8941  zfac  9282  zfcndac  9441  addsrmo  9894  mulsrmo  9895  cotr2g  13715  isirred2  18701  rmo4fOLD  29336  bnj580  30983  bnj978  31019  axacprim  31584  dfso2  31644  dfpo2  31645  dfon2lem8  31695  dffun10  32021  wl-sbcom2d  33344  mpt2bi123f  33971  3albii  34012  ssrel3  34067  inxpss  34082  inxpss3  34084  dford4  37596  isdomn3  37782  undmrnresiss  37910  cnvssco  37912  ntrneikb  38392  ntrneixb  38393  pm14.12  38622