Theorem 2albii 1481

Description: Inference adding 2 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 1480	. 2 |- ( A. y ph <-> A. y ps )
3	2	albii 1480	1 |- ( A. x A. y ph <-> A. x A. y ps )

Syntax hints:   <-> wb 105   A.wal 1361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2078  mo4f  2096  moanim  2110  2eu4  2129  ralcomf  2648  raliunxp  4780  cnvsym  5024  intasym  5025  intirr  5027  codir  5029  qfto  5030  dffun4  5239  dffun4f  5244  funcnveq  5291  fun11  5295  fununi  5296  mpo2eqb  5998  addnq0mo  7460  mulnq0mo  7461  addsrmo  7756  mulsrmo  7757