Theorem 2albii 1520

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

Syntax hints:   ↔ wb 105  ∀wal 1396

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 1496  ax-gen 1498

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2122  mo4f  2140  moanim  2154  2eu4  2173  ralcomf  2695  raliunxp  4877  cnvsym  5127  intasym  5128  intirr  5130  codir  5132  qfto  5133  dffun4  5344  dffun4f  5349  funcnveq  5400  fun11  5404  fununi  5405  mpo2eqb  6141  addnq0mo  7710  mulnq0mo  7711  addsrmo  8006  mulsrmo  8007