Theorem 2albii 1482

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

Syntax hints:   ↔ wb 105  ∀wal 1362

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 1458  ax-gen 1460

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2080  mo4f  2098  moanim  2112  2eu4  2131  ralcomf  2651  raliunxp  4789  cnvsym  5033  intasym  5034  intirr  5036  codir  5038  qfto  5039  dffun4  5249  dffun4f  5254  funcnveq  5301  fun11  5305  fununi  5306  mpo2eqb  6010  addnq0mo  7481  mulnq0mo  7482  addsrmo  7777  mulsrmo  7778