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  4803  cnvsym  5049  intasym  5050  intirr  5052  codir  5054  qfto  5055  dffun4  5265  dffun4f  5270  funcnveq  5317  fun11  5321  fununi  5322  mpo2eqb  6028  addnq0mo  7507  mulnq0mo  7508  addsrmo  7803  mulsrmo  7804