Theorem 2albii 1471

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

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

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 1447  ax-gen 1449

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2068  mo4f  2086  moanim  2100  2eu4  2119  ralcomf  2638  raliunxp  4766  cnvsym  5010  intasym  5011  intirr  5013  codir  5015  qfto  5016  dffun4  5225  dffun4f  5230  funcnveq  5277  fun11  5281  fununi  5282  mpo2eqb  5980  addnq0mo  7442  mulnq0mo  7443  addsrmo  7738  mulsrmo  7739