Theorem 2albii 1495

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

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

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 1471  ax-gen 1473

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2098  mo4f  2116  moanim  2130  2eu4  2149  ralcomf  2669  raliunxp  4837  cnvsym  5085  intasym  5086  intirr  5088  codir  5090  qfto  5091  dffun4  5301  dffun4f  5306  funcnveq  5356  fun11  5360  fununi  5361  mpo2eqb  6078  addnq0mo  7595  mulnq0mo  7596  addsrmo  7891  mulsrmo  7892