Theorem 2albii 1464

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

Syntax hints:   ↔ wb 104  ∀wal 1346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mor  2061  mo4f  2079  moanim  2093  2eu4  2112  ralcomf  2631  raliunxp  4750  cnvsym  4992  intasym  4993  intirr  4995  codir  4997  qfto  4998  dffun4  5207  dffun4f  5212  funcnveq  5259  fun11  5263  fununi  5264  mpo2eqb  5960  addnq0mo  7402  mulnq0mo  7403  addsrmo  7698  mulsrmo  7699