Theorem 2albii 1495

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

Syntax hints:   ↔ wb 105  ∀wal 1371

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 1471  ax-gen 1473

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2097  mo4f  2115  moanim  2129  2eu4  2148  ralcomf  2668  raliunxp  4827  cnvsym  5075  intasym  5076  intirr  5078  codir  5080  qfto  5081  dffun4  5291  dffun4f  5296  funcnveq  5346  fun11  5350  fununi  5351  mpo2eqb  6068  addnq0mo  7580  mulnq0mo  7581  addsrmo  7876  mulsrmo  7877