Theorem 2albii 1827

Description: Inference adding two 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 1826	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1826	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Syntax hints:   ↔ wb 205  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  sbcom2  2165  2sb6rf  2475  mo4f  2569  2mo2  2651  2mos  2653  r3al  3128  ralcom  3283  ralcomf  3285  nfnid  5302  raliunxp  5747  cnvsym  6018  intasym  6019  intirr  6022  codir  6024  qfto  6025  dfpo2  6198  dffun4  6444  fun11  6506  fununi  6507  mpo2eqb  7400  aceq0  9875  zfac  10217  zfcndac  10376  addsrmo  10830  mulsrmo  10831  cotr2g  14685  isirred2  19941  bnj580  32889  bnj978  32925  axacprim  33644  dfso2  33718  dfon2lem8  33762  frpoins3xpg  33783  frpoins3xp3g  33784  dffun10  34212  wl-sbcom2d  35712  mpobi123f  36316  3albii  36383  ssrel3  36430  inxpss  36443  inxpss3  36445  trcoss2  36598  dford4  40848  isdomn3  41026  undmrnresiss  41182  cnvssco  41184  pm14.12  42009  ichn  44877  dfich2  44879  ichcom  44880  ichbi12i  44881