Theorem 2albii 1360

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 1359	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1359	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Syntax hints:   ↔ wb 98  ∀wal 1241

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 1336  ax-gen 1338

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  mor  1942  mo4f  1960  moanim  1974  2eu4  1993  ralcomf  2471  raliunxp  4477  cnvsym  4708  intasym  4709  intirr  4711  codir  4713  qfto  4714  dffun4  4913  dffun4f  4918  funcnveq  4962  fun11  4966  fununi  4967  mpt22eqb  5610  addnq0mo  6545  mulnq0mo  6546  addsrmo  6828  mulsrmo  6829