Theorem 2albii 1820

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

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  3albii  1821  sbcom2  2173  2sb6rf  2478  mo4f  2567  2mo2  2647  2mos  2649  2mosOLD  2650  r3al  3197  ralcom  3289  ralcomf  3302  sbccomlem  3869  nfnid  5375  ssrel3  5796  raliunxp  5850  cnvsym  6132  cnvsymOLD  6133  cnvsymOLDOLD  6134  intasym  6135  intirr  6138  codir  6140  qfto  6141  dfpo2  6316  dffun4  6577  fun11  6640  fununi  6641  mpo2eqb  7565  frpoins3xpg  8165  xpord3inddlem  8179  aceq0  10158  zfac  10500  zfcndac  10659  addsrmo  11113  mulsrmo  11114  cotr2g  15015  isirred2  20421  isdomn3  20715  bnj580  34927  bnj978  34963  axacprim  35707  dfso2  35755  dfon2lem8  35791  dffun10  35915  wl-sbcom2d  37562  mpobi123f  38169  r2alan  38250  inxpss  38312  inxpss3  38315  cnvref5  38352  trcoss2  38485  dfantisymrel5  38763  antisymrelres  38764  dford4  43041  undmrnresiss  43617  cnvssco  43619  pm14.12  44440  ichn  47443  dfich2  47445  ichcom  47446  ichbi12i  47447