Theorem 2albii 1357

Description: Inference adding 2 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 1356	. 2 ⊢ (∀yφ ↔ ∀yψ)
3	2	albii 1356	1 ⊢ (∀x∀yφ ↔ ∀x∀yψ)

Syntax hints:   ↔ wb 98  ∀wal 1240

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  mor  1939  mo4f  1957  moanim  1971  2eu4  1990  ralcomf  2465  raliunxp  4420  cnvsym  4651  intasym  4652  intirr  4654  codir  4656  qfto  4657  dffun4  4856  dffun4f  4861  funcnveq  4905  fun11  4909  fununi  4910  mpt22eqb  5552  addnq0mo  6430  mulnq0mo  6431  addsrmo  6671  mulsrmo  6672