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  2174  2sb6rf  2478  mo4f  2567  2mo2  2647  2mos  2649  2mosOLD  2650  r3al  3183  ralcom  3274  ralcomf  3286  sbccomlem  3849  nfnid  5350  ssrel3  5770  raliunxp  5824  cnvsym  6106  cnvsymOLD  6107  cnvsymOLDOLD  6108  intasym  6109  intirr  6112  codir  6114  qfto  6115  dfpo2  6290  dffun4  6552  fun11  6615  fununi  6616  mpo2eqb  7544  frpoins3xpg  8144  xpord3inddlem  8158  aceq0  10137  zfac  10479  zfcndac  10638  addsrmo  11092  mulsrmo  11093  cotr2g  15000  isirred2  20386  isdomn3  20680  bnj580  34949  bnj978  34985  axacprim  35729  dfso2  35777  dfon2lem8  35813  dffun10  35937  wl-sbcom2d  37584  mpobi123f  38191  r2alan  38272  inxpss  38334  inxpss3  38337  cnvref5  38374  trcoss2  38507  dfantisymrel5  38785  antisymrelres  38786  dford4  43020  undmrnresiss  43595  cnvssco  43597  pm14.12  44412  ichn  47437  dfich2  47439  ichcom  47440  ichbi12i  47441