Theorem 2albii 1524

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	⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Proof of Theorem 2albii

Step	Hyp	Ref	Expression
1		albii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	albii 1523	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1523	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Syntax hints:   ↔ wb 105  ∀wal 1400

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 1500  ax-gen 1502

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2129  mo4f  2147  moanim  2161  2eu4  2180  ralcomf  2712  raliunxp  4916  cnvsym  5166  intasym  5167  intirr  5169  codir  5171  qfto  5172  dffun4  5383  dffun4f  5388  funcnveq  5439  fun11  5443  fununi  5444  mpo2eqb  6188  addnq0mo  7804  mulnq0mo  7805  addsrmo  8100  mulsrmo  8101