Theorem 2albii 1405

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

Syntax hints:   ↔ wb 103  ∀wal 1287

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mor  1990  mo4f  2008  moanim  2022  2eu4  2041  ralcomf  2528  raliunxp  4577  cnvsym  4815  intasym  4816  intirr  4818  codir  4820  qfto  4821  dffun4  5026  dffun4f  5031  funcnveq  5077  fun11  5081  fununi  5082  mpt22eqb  5754  addnq0mo  7006  mulnq0mo  7007  addsrmo  7289  mulsrmo  7290