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  4819  cnvsym  5066  intasym  5067  intirr  5069  codir  5071  qfto  5072  dffun4  5282  dffun4f  5287  funcnveq  5337  fun11  5341  fununi  5342  mpo2eqb  6055  addnq0mo  7560  mulnq0mo  7561  addsrmo  7856  mulsrmo  7857