Theorem 2albii 1400

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

Syntax hints:   <-> wb 103   A.wal 1282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mor  1983  mo4f  2001  moanim  2015  2eu4  2034  ralcomf  2515  raliunxp  4495  cnvsym  4728  intasym  4729  intirr  4731  codir  4733  qfto  4734  dffun4  4933  dffun4f  4938  funcnveq  4982  fun11  4986  fununi  4987  mpt22eqb  5630  addnq0mo  6637  mulnq0mo  6638  addsrmo  6920  mulsrmo  6921