Theorem 2albii 1447

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

Syntax hints:   ↔ wb 104  ∀wal 1329

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 1423  ax-gen 1425

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mor  2039  mo4f  2057  moanim  2071  2eu4  2090  ralcomf  2590  raliunxp  4675  cnvsym  4917  intasym  4918  intirr  4920  codir  4922  qfto  4923  dffun4  5129  dffun4f  5134  funcnveq  5181  fun11  5185  fununi  5186  mpo2eqb  5873  addnq0mo  7248  mulnq0mo  7249  addsrmo  7544  mulsrmo  7545