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	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
2albii	⊢ (∀x∀yφ ↔ ∀x∀yψ)

Proof of Theorem 2albii

Step	Hyp	Ref	Expression
1		albii.1	. . 3 ⊢ (φ ↔ ψ)
2	1	albii 1566	. 2 ⊢ (∀yφ ↔ ∀yψ)
3	2	albii 1566	1 ⊢ (∀x∀yφ ↔ ∀x∀yψ)

Syntax hints:   ↔ wb 176  ∀wal 1540

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  2769  axcnvprim  4091  axssetprim  4092  axsiprim  4093  axins2prim  4095  axins3prim  4096  ssrelk  4211  eqrelk  4212  cnvkexg  4286  ssetkex  4294  sikexlem  4295  sikexg  4296  insklem  4304  ins2kexg  4305  ins3kexg  4306  raliunxp  4823  ssopr  4846  cnvsym  5027  intasym  5028  intirr  5029  dffun2  5119  dffun4  5121  fun11  5159  fununi  5160  enmap2lem4  6066  enmap1lem4  6072