Theorem 2albii 1459

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

Syntax hints:   ↔ wb 104  ∀wal 1341

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 1435  ax-gen 1437

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mor  2056  mo4f  2074  moanim  2088  2eu4  2107  ralcomf  2627  raliunxp  4745  cnvsym  4987  intasym  4988  intirr  4990  codir  4992  qfto  4993  dffun4  5199  dffun4f  5204  funcnveq  5251  fun11  5255  fununi  5256  mpo2eqb  5951  addnq0mo  7388  mulnq0mo  7389  addsrmo  7684  mulsrmo  7685