Theorem 2albii 1485

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 1484	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1484	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 1461  ax-gen 1463

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2087  mo4f  2105  moanim  2119  2eu4  2138  ralcomf  2658  raliunxp  4808  cnvsym  5054  intasym  5055  intirr  5057  codir  5059  qfto  5060  dffun4  5270  dffun4f  5275  funcnveq  5322  fun11  5326  fununi  5327  mpo2eqb  6036  addnq0mo  7531  mulnq0mo  7532  addsrmo  7827  mulsrmo  7828