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  4807  cnvsym  5053  intasym  5054  intirr  5056  codir  5058  qfto  5059  dffun4  5269  dffun4f  5274  funcnveq  5321  fun11  5325  fununi  5326  mpo2eqb  6032  addnq0mo  7514  mulnq0mo  7515  addsrmo  7810  mulsrmo  7811