Theorem 2albii 1471

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

Syntax hints:   ↔ wb 105  ∀wal 1351

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 1447  ax-gen 1449

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2068  mo4f  2086  moanim  2100  2eu4  2119  ralcomf  2638  raliunxp  4769  cnvsym  5013  intasym  5014  intirr  5016  codir  5018  qfto  5019  dffun4  5228  dffun4f  5233  funcnveq  5280  fun11  5284  fununi  5285  mpo2eqb  5984  addnq0mo  7446  mulnq0mo  7447  addsrmo  7742  mulsrmo  7743