Theorem 2albii 1519

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

Syntax hints:   ↔ wb 105  ∀wal 1395

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 1495  ax-gen 1497

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2122  mo4f  2140  moanim  2154  2eu4  2173  ralcomf  2694  raliunxp  4871  cnvsym  5120  intasym  5121  intirr  5123  codir  5125  qfto  5126  dffun4  5337  dffun4f  5342  funcnveq  5393  fun11  5397  fununi  5398  mpo2eqb  6130  addnq0mo  7666  mulnq0mo  7667  addsrmo  7962  mulsrmo  7963