Theorem 2albii 1494

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 1493	. 2 |- ( A. y ph <-> A. y ps )
3	2	albii 1493	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 1470  ax-gen 1472

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2096  mo4f  2114  moanim  2128  2eu4  2147  ralcomf  2667  raliunxp  4820  cnvsym  5067  intasym  5068  intirr  5070  codir  5072  qfto  5073  dffun4  5283  dffun4f  5288  funcnveq  5338  fun11  5342  fununi  5343  mpo2eqb  6057  addnq0mo  7562  mulnq0mo  7563  addsrmo  7858  mulsrmo  7859