Theorem 2albii 1567

Description: Inference adding two 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.xA.yph <-> A.xA.yps)

Proof of Theorem 2albii

Step	Hyp	Ref	Expression
1		albii.1	. . 3 |- (ph <-> ps)
2	1	albii 1566	. 2 |- (A.yph <-> A.yps)
3	2	albii 1566	1 |- (A.xA.yph <-> A.xA.yps)

Syntax hints:   <-> wb 176  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  mo4f  2236  2mos  2283  2eu4  2287  2eu6  2289  ralcomf  2770  axcnvprim  4092  axssetprim  4093  axsiprim  4094  axins2prim  4096  axins3prim  4097  ssrelk  4212  eqrelk  4213  cnvkexg  4287  ssetkex  4295  sikexlem  4296  sikexg  4297  insklem  4305  ins2kexg  4306  ins3kexg  4307  raliunxp  4824  ssopr  4847  cnvsym  5028  intasym  5029  intirr  5030  dffun2  5120  dffun4  5122  fun11  5160  fununi  5161  enmap2lem4  6067  enmap1lem4  6073