Theorem 2albii 1464

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

Syntax hints:   ↔ wb 104  ∀wal 1346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mor  2061  mo4f  2079  moanim  2093  2eu4  2112  ralcomf  2631  raliunxp  4752  cnvsym  4994  intasym  4995  intirr  4997  codir  4999  qfto  5000  dffun4  5209  dffun4f  5214  funcnveq  5261  fun11  5265  fununi  5266  mpo2eqb  5962  addnq0mo  7409  mulnq0mo  7410  addsrmo  7705  mulsrmo  7706