Theorem 2albii 1517

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

Syntax hints:   ↔ wb 105  ∀wal 1393

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2120  mo4f  2138  moanim  2152  2eu4  2171  ralcomf  2692  raliunxp  4863  cnvsym  5112  intasym  5113  intirr  5115  codir  5117  qfto  5118  dffun4  5329  dffun4f  5334  funcnveq  5384  fun11  5388  fununi  5389  mpo2eqb  6120  addnq0mo  7645  mulnq0mo  7646  addsrmo  7941  mulsrmo  7942