Theorem 2albii 1520

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

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

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 1496  ax-gen 1498

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2125  mo4f  2143  moanim  2157  2eu4  2176  ralcomf  2706  raliunxp  4898  cnvsym  5148  intasym  5149  intirr  5151  codir  5153  qfto  5154  dffun4  5365  dffun4f  5370  funcnveq  5421  fun11  5425  fununi  5426  mpo2eqb  6165  addnq0mo  7764  mulnq0mo  7765  addsrmo  8060  mulsrmo  8061