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  2084  mo4f  2102  moanim  2116  2eu4  2135  ralcomf  2655  raliunxp  4804  cnvsym  5050  intasym  5051  intirr  5053  codir  5055  qfto  5056  dffun4  5266  dffun4f  5271  funcnveq  5318  fun11  5322  fununi  5323  mpo2eqb  6029  addnq0mo  7509  mulnq0mo  7510  addsrmo  7805  mulsrmo  7806